proposition: Lemma Rmult_integral_contrapositive : forall r1 r2, r1 <> 0 /\ r2 <> 0 -> r1 * r2 <> 0.
proof: Proof. now intros r1 r2 [H1 H2] [r10 | r20]%Rmult_integral. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField