induction b with
| zero =>
  intro c h
  rw [mul_zero] at h
  apply Eq.symm
  show c = 0
  cases eq_zero_or_eq_zero_of_mul_eq_zero (Eq.symm h) with
  | inl ha0 => contradiction
  | inr hc0 => assumption
| succ b' ihb =>
  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
a b : Nat
ha : a ≠ zero
⊢ ∀ (c : Nat), a * b = a * c → b = c
no goals