proposition: Lemma Zmult_intro_lft : forall a b c : Z, a <> 0%Z -> (a * b)%Z = (a * c)%Z -> b = c.
proof: Proof. intros a b c Ha Habc. cut ((b - c)%Z = 0%Z); auto with zarith. elim (Zmult_zero_div a (b - c)). intro; elim Ha; assumption. tauto. rewrite Zmult_comm; rewrite BinInt.Zmult_minus_distr_r; rewrite (Zmult_comm b a); rewrite (Zmult_comm c a). auto with zarith. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)