proposition: Lemma Zmult_no_zero_div : forall a b : Z, a <> 0%Z -> b <> 0%Z -> (a * b)%Z <> 0%Z.
proof: Proof. intros a b Ha Hb. intro Hfalse. generalize (Zmult_zero_div a b Hfalse). tauto. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)