proposition: Lemma Rmult_pos_cases : forall r1 r2, r1 * r2 > 0 -> (r1 > 0 /\ r2 > 0) \/ (r1 < 0 /\ r2 < 0).
proof: Proof. intros r1 r2. destruct (Rtotal_order r1 0) as [Hlt1 | [-> | Hgt1]]; cycle 1. - now intros H; exfalso; rewrite Rmult_0_l in H; apply (Rlt_irrefl 0). - destruct (Rtotal_order r2 0) as [Hlt2 | [-> | Hgt2]]; cycle 1. + now intros H; exfalso; rewrite Rmult_0_r in H; apply (Rlt_irrefl 0). + now intros _; left. + intros H; exfalso; apply (Rgt_not_le (r1 * r2) 0); try easy. now left; apply Rmult_pos_neg. - destruct (Rtotal_order r2 0) as [Hlt2 | [-> | Hgt2]]; cycle 1. + now intros H; exfalso; rewrite Rmult_0_r in H; apply (Rlt_irrefl 0). + intros H; exfalso; apply (Rgt_not_le (r1 * r2) 0); try easy. now left; apply Rmult_neg_pos. + now intros _; right. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField