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