proposition: Lemma CRle_trans : forall x y z, (x <= y -> y <= z -> x <= z)%CR.
proof: Proof. intros x y z H1 H2. unfold CRle. rewrite <- (doubleSpeed_Eq (z-x)%CR). intros e. assert (H1':=H1 ((1#2)*e)%Qpos). assert (H2':=H2 ((1#2)*e)%Qpos). clear H1 H2. simpl in *. unfold Cap_raw in *. simpl in *. apply (Qle_trans _ ((approximate z ((1 # 2) * ((1 # 2) * e))%Qpos - approximate y ((1 # 2) * ((1 # 2) * e))%Qpos + (approximate y ((1 # 2) * ((1 # 2) * e))%Qpos - approximate x ((1 # 2) * ((1 # 2) * e))%Qpos)))). 2: ring_simplify; apply Qle_refl. apply (Qle_trans _ (-(1#2)*proj1_sig e + - (1#2)* proj1_sig e)). ring_simplify. apply Qmult_le_r. apply Qpos_ispos. discriminate. apply Qplus_le_compat; apply (Qle_trans _ (- ((1 # 2) * ` e))). destruct e. simpl. ring_simplify. apply Qle_refl. assumption. destruct e. simpl. ring_simplify. apply Qle_refl. assumption. Qed.
imports: QArith Qabs CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.metric2.CRmetric CoRN.model.totalorder.QMinMax CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric CoRN.stdlib_omissions.Pair MathClasses.interfaces.canonical_names