proposition: Lemma Rdiv_neg_neg : forall r1 r2, r1 < 0 -> r2 < 0 -> r1 / r2 > 0.
proof: Proof. now unfold Rdiv; intros r1 r2 H H'%Rinv_neg; apply Rmult_neg_neg. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField