mul_left_cancel

theorem mul_left_cancel (a b c : mynat) (ha : a ≠ 0) : a * b = a * c → b = c := begin

revert a b,
induction c,
intros a b ha h,
cases a,
exfalso,
exact ha (refl 0),
rw mul_zero at h,
rw succ_mul at h,
apply add_left_eq_zero h,

intros a e ha h,
cases e,
exfalso,
rw mul_zero at h,
rw mul_succ at h,
symmetry at h,
exact ha (add_left_eq_zero h),

rw mul_succ at h,
rw mul_succ at h,
have h := add_right_cancel _ a _ h,
apply succ_eq_succ_of_eq,
exact c_ih a e ha h,

end