proposition: Lemma Zsimpl_mult_l : forall n m p : Z, n <> 0%Z -> (n * m)%Z = (n * p)%Z -> m = p.
proof: Proof. intros. apply Zplus_reg_l with (n := (- p)%Z). replace (- p + p)%Z with 0%Z. apply Zmult_integral_l with (n := n). assumption. replace ((- p + m) * n)%Z with (n * m + - (n * p))%Z. apply Zegal_left. assumption. ring. ring. Qed.
imports: Coq(Lia)