intro
| zero =>
  intro h
  rw [mul_zero] at h
  cases eq_zero_or_eq_zero_of_mul_eq_zero h with
  | inl ha => contradiction
  | inr hb => assumption  | succ c' =>
  intro h
  apply succ_eq_succ_of_eq
  show b' = c'
  rw [mul_succ, mul_succ] at h
  have habax : a*b' = a*c' := add_right_cancel h
  have ihbc : a*b' = a*c' → b' = c' := ihb c'
  apply ihbc
  exact habax
case succ
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
⊢ ∀ (c : Nat), a * succ b' = a * c → succ b' = c
no goals