proposition: Lemma Rmult_neg_cases : forall r1 r2, r1 * r2 < 0 -> (r1 > 0 /\ r2 < 0) \/ (r1 < 0 /\ r2 > 0).
proof: Proof. intros r1 r2 H%Ropp_lt_contravar%Rlt_gt. rewrite Ropp_0, Ropp_mult_distr_l in H. apply Rmult_pos_cases in H as [[H1%Ropp_lt_contravar H2] | [H1%Ropp_lt_contravar H2]]. - now right; split; [| assumption]; rewrite Ropp_involutive, Ropp_0 in H1. - now left; split; [| assumption]; rewrite Ropp_involutive, Ropp_0 in H1. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField