proposition: Lemma Rmult_eq_0_compat : forall r1 r2, r1 = 0 \/ r2 = 0 -> r1 * r2 = 0.
proof: Proof. now intros r1 r2 [-> | ->]; [apply Rmult_0_l | apply Rmult_0_r]. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField