proposition: Lemma Zmult_intro_rht : forall a b c : Z, a <> 0%Z -> (b * a)%Z = (c * a)%Z -> b = c.
proof: Proof. intros a b c. rewrite (Zmult_comm b a); rewrite (Zmult_comm c a); apply Zmult_intro_lft. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)