proposition: Lemma Rmult_div_l : forall r1 r2, r2 <> 0 -> r1 * r2 / r2 = r1.
proof: Proof. now unfold Rdiv; intros r1 r2 H; rewrite Rmult_assoc, Rinv_r, Rmult_1_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField