proposition: Lemma Rdiv_eq_compat_l : forall r r1 r2, r1 = r2 -> r / r1 = r / r2.
proof: Proof. now unfold Rdiv; intros r r1 r2 H%Rinv_eq_compat; apply Rmult_eq_compat_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField