proposition: Lemma Rmult_div_swap : forall r1 r2 r3, r1 * r2 / r3 = r1 / r3 * r2.
proof: Proof. unfold Rdiv; intros r1 r2 r3. now rewrite Rmult_assoc, (Rmult_comm r2), <-Rmult_assoc. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField