proposition: Lemma CRmult_assoc_xfactor_le : forall (x y z : CR), let b := ((CR_b (1#1) x + (1#1)) * (CR_b (1#1) y + (1#1)) * (CR_b (1#1) z + (1#1)))%Qpos in (` (CR_b (1 ↾ eq_refl) x) + 1 <= ` b)%Q.
proof: Proof. intros. unfold b. simpl. rewrite <- Qmult_assoc, Qmult_comm. rewrite <- Qmult_1_l, <- Qmult_1_l at 1. rewrite Qmult_assoc. apply Qmult_le_compat_r. apply (Qpos_mult_le_compat (1#1) (1#1)). rewrite <- Qplus_0_l. apply Qplus_le_l, (Qpos_nonneg (CR_b (1#1) y)). rewrite <- Qplus_0_l. apply Qplus_le_l, (Qpos_nonneg (CR_b (1#1) z)). rewrite <- Qplus_assoc. apply (Qle_trans _ (0+2)). discriminate. apply Qplus_le_l. apply Qabs_nonneg. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names