proposition: Lemma Rmult_integral : forall r1 r2, r1 * r2 = 0 -> r1 = 0 \/ r2 = 0.
proof: Proof. intros; destruct (Req_dec r1 0) as [Hz | Hnz]; [left | right]; try easy. apply (Rmult_eq_compat_l (/ r1)) in H. now rewrite <-Rmult_assoc, Rinv_l, Rmult_1_l, Rmult_0_r in H. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField