proposition: Lemma CRmult_le_0_compat : forall {R : ConstructiveReals} (a b : CRcarrier R), 0 <= a -> 0 <= b -> 0 <= a * b.
proof: Proof. intros. intro abs. assert (0 < -(a*b)) as epsPos. { rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. exact abs. } destruct (CR_archimedean R (b * ((/ -(a*b)) (inr epsPos)))) as [n maj]. assert (0 < CR_of_Q R (Z.pos n #1)) as nPos. { apply CR_of_Q_lt. reflexivity. } assert (b * (/ CR_of_Q R (Z.pos n #1)) (inr nPos) < -(a*b)). { apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n #1))). - apply nPos. - rewrite <- (Rmul_assoc (CRisRing R)), CRinv_l, CRmult_1_r. apply (CRmult_lt_compat_r (-(a*b))) in maj. + rewrite CRmult_assoc, CRinv_l, CRmult_1_r in maj. rewrite CRmult_comm. apply maj. + apply epsPos. } pose proof (CRmult_le_compat_l_half (a + (/ CR_of_Q R (Z.pos n #1)) (inr nPos)) 0 b). assert (0 + 0 < a + (/ CR_of_Q R (Z.pos n #1)) (inr nPos)). { apply CRplus_le_lt_compat. - apply H. - apply CRinv_0_lt_compat. apply nPos. } rewrite CRplus_0_l in H3. specialize (H2 H3 H0). clear H3. rewrite CRmult_0_r in H2. apply H2. clear H2. rewrite (Rdistr_l (CRisRing R)). apply (CRplus_lt_compat_l R (a*b)) in H1. rewrite CRplus_opp_r in H1. rewrite (CRmult_comm ((/ CR_of_Q R (Z.pos n # 1)) (inr nPos))). apply H1. Qed.
imports: QArith Qabs Qround