proposition: Lemma Ropp_div_distr_r : forall r1 r2, r1 / - r2 = - (r1 / r2).
proof: Proof. now unfold Rdiv; intros r1 r2; rewrite Ropp_mult_distr_r, Rinv_opp. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField