proposition: Lemma Rmult_neq_0_reg : forall r1 r2, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0.
proof: Proof. intros r1 r2 H; split; intros Heq0; rewrite Heq0 in H. - now rewrite Rmult_0_l in H. - now rewrite Rmult_0_r in H. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField