proposition: Lemma Rdiv_lt_0_compat : forall a b, 0 < a -> 0 < b -> 0 < a / b.
proof: Proof. intros r1 r2 r1_pos r2_pos. now apply (Rmult_lt_0_compat r1 (/ r2) r1_pos), Rinv_0_lt_compat. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField