proposition: Lemma Rdiv_pos_cases : forall r1 r2 : R, r1 / r2 > 0 -> r1 > 0 /\ r2 > 0 \/ r1 < 0 /\ r2 < 0.
proof: Proof. unfold Rdiv; intros r1 r2 [[I J%Rinv_pos] | [I J%Rinv_neg]]%Rmult_pos_cases. - now left; rewrite Rinv_inv in J. - now right; rewrite Rinv_inv in J. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField