proposition: Lemma CRmin_glb: forall x y z : CR, (z <= x -> z <= y -> z <= CRmin x y)%CR.
proof: Proof. intros x y z Hx Hy. rewrite <- (doubleSpeed_Eq z) in * |- *. intros e. assert (Hx':=Hx ((1#2)*e)%Qpos). assert (Hy':=Hy ((1#2)*e)%Qpos). clear Hx Hy. simpl in *. unfold Cap_raw in *. simpl in *. unfold Cap_raw. simpl. apply (Qle_trans _ ((-(1#2)*proj1_sig e) + (- (1#2)*proj1_sig e))). ring_simplify. apply Qmult_le_r. apply Qpos_ispos. discriminate. apply (Qle_trans _ ((approximate z ((1#2)*((1 # 2) * ((1 # 2) * e)))%Qpos + - approximate z ((1#2)*((1 # 2) * e))%Qpos) + (Qmin (approximate x ((1 # 2) * ((1 # 2) * e))%Qpos) (approximate y ((1 # 2) * ((1 # 2) * e))%Qpos) + - approximate z ((1#2)*((1 # 2) * ((1 # 2) * e)))%Qpos))). 2: ring_simplify; rewrite Qplus_comm; apply Qle_refl. apply Qplus_le_compat. - apply (Qle_trans _ (- ((1 # 2) * ` e))). destruct e; simpl; ring_simplify; apply Qle_refl. cut (ball ((1#2)*proj1_sig e) (approximate z ((1#2)*((1 # 2) * ((1 # 2) * e)))%Qpos) (approximate z ((1#2)*((1 # 2) * e))%Qpos)) ;[intros [A B]; assumption|]. refine (ball_weak_le _ _ _ _ _). 2:apply regFun_prf. rewrite -> Qle_minus_iff. simpl. ring_simplify. apply (Qpos_nonneg ((8#64)*e)). - apply (Qle_trans _ (- ((1 # 2) * ` e))). destruct e; simpl; ring_simplify; apply Qle_refl. apply Qmin_case;intro;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