proposition: Lemma CRmult_le_0_compat : forall a b : CR, (0 <= a)%CR -> (0 <= b)%CR -> (0 <= a*b)%CR.
proof: Proof. intros. pose (Qpos_max (CR_b (1#1) a) (CR_b (1#1) b)) as c. assert (' (- ` c)%Q <= a)%CR as alower. { apply (@CRle_trans _ (' (-proj1_sig (CR_b (1#1) a))%Q)). 2: apply (CR_b_lowerBound _ _). apply CRle_Qle. apply Qopp_le_compat, Qpos_max_ub_l. } assert (a <= '(` c)%Q)%CR as aupper. { apply (@CRle_trans _ (' (proj1_sig (CR_b (1#1) a))) _ (CR_b_upperBound _ _)). apply CRle_Qle. apply Qpos_max_ub_l. } assert (' (- ` c)%Q <= b)%CR as blower. { apply (@CRle_trans _ (' (-proj1_sig (CR_b (1#1) b))%Q)). 2: apply (CR_b_lowerBound _ _). apply CRle_Qle. apply Qopp_le_compat, Qpos_max_ub_r. } assert (b <= '(` c)%Q)%CR as bupper. { apply (@CRle_trans _ (' (proj1_sig (CR_b (1#1) b))) _ (CR_b_upperBound _ _)). apply CRle_Qle. apply Qpos_max_ub_r. } unfold CRle in H0. rewrite CRopp_0, CRplus_0_r in H0. unfold CRle in H. rewrite CRopp_0, CRplus_0_r in H. rewrite <- (@CRboundAbs_Eq c a) in H. 2: exact alower. 2: exact aupper. rewrite <- (@CRboundAbs_Eq c b) in H0. 2: exact blower. 2: exact bupper. rewrite <- (CRmult_bounded_mult c). 2: exact blower. 2: exact bupper. change (0 <= ucFun2 (CRmult_bounded c) a b)%CR. rewrite <- (@CRboundAbs_Eq c a). rewrite <- (@CRboundAbs_Eq c b). apply (CRmult_le_0_compat_bounded (CRboundAbs c a) (CRboundAbs c b) c). - exact H0. - exact H. - intros. apply Qmax_ub_l. - intros. simpl. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. - intros. apply Qmax_ub_l. - intros. simpl. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. - exact blower. - exact bupper. - exact alower. - exact aupper. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders