proposition: Lemma CReal_mult_le_0_compat : forall (a b : CReal), 0 <= a -> 0 <= b -> 0 <= a * b.
proof: Proof. intros. intro abs. assert (0 < -(a*b)) as epsPos. { rewrite <- CReal_opp_0. apply CReal_opp_gt_lt_contravar. exact abs. } destruct (Rup_nat (b * (/ (-(a*b))) (inr epsPos))) as [n maj]. destruct n as [|n]. - apply (CReal_mult_lt_compat_r (-(a*b))) in maj. + rewrite CReal_mult_0_l, CReal_mult_assoc, CReal_inv_l, CReal_mult_1_r in maj. contradiction. + exact epsPos. - assert (0 < inject_Q (Z.of_nat (S n) #1)) as nPos. { apply inject_Q_lt. unfold Qlt, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Z2Nat.inj_lt. - discriminate. - apply Zle_0_nat. - rewrite Nat2Z.id. apply -> Nat.succ_le_mono; apply Nat.le_0_l. } assert (b * (/ inject_Q (Z.of_nat (S n) #1)) (inr nPos) < -(a*b)). { apply (CReal_mult_lt_reg_r (inject_Q (Z.of_nat (S n) #1))). { apply nPos. } rewrite CReal_mult_assoc, CReal_inv_l, CReal_mult_1_r. apply (CReal_mult_lt_compat_r (-(a*b))) in maj. - rewrite CReal_mult_assoc, CReal_inv_l, CReal_mult_1_r in maj. rewrite CReal_mult_comm. apply maj. - apply epsPos. } pose proof (CReal_mult_le_compat_l_half (a + (/ inject_Q (Z.of_nat (S n) #1)) (inr nPos)) 0 b). assert (0 + 0 < a + (/ inject_Q (Z.of_nat (S n) #1)) (inr nPos)). { apply CReal_plus_le_lt_compat. { apply H. } apply CReal_inv_0_lt_compat. apply nPos. } rewrite CReal_plus_0_l in H3. specialize (H2 H3 H0). clear H3. rewrite CReal_mult_0_r in H2. apply H2. clear H2. rewrite CReal_mult_plus_distr_r. apply (CReal_plus_lt_compat_l (a*b)) in H1. rewrite CReal_plus_opp_r in H1. rewrite (CReal_mult_comm ((/ inject_Q (Z.of_nat (S n) #1)) (inr nPos))). apply H1. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra