proposition: Lemma CRmax_boundBelow : forall (a:Q) (y:CR), (CRmax (' a) y == boundBelow a y)%CR.
proof: Proof. intros a y. unfold ucFun2, CRmax. unfold Cmap2. unfold inject_Q_CR. intros e1 e2. destruct y; simpl; unfold Cmap_fun, Cap_fun, Cap_raw; simpl. specialize (regFun_prf ((1 # 2) * e1)%Qpos e2). apply AbsSmall_Qabs. apply (Qle_trans _ _ _ (Qmax_contract _ _ _)). apply AbsSmall_Qabs in regFun_prf. apply (Qle_trans _ _ _ regFun_prf). apply Qplus_le_l. simpl. rewrite <- (Qmult_1_l (proj1_sig e1)) at 2. rewrite Qplus_0_r. apply Qmult_le_r. apply Qpos_ispos. discriminate. 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