proposition: Lemma CRmin_boundAbove : forall (a:Q) (y:CR), (CRmin (' a) y == boundAbove a y)%CR.
proof: Proof. intros a y. unfold ucFun2, CRmin. 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). rewrite Qplus_0_r. split. - apply Qmin_case. intros. apply Qmin_case. intros. unfold Qminus. rewrite Qplus_opp_r. apply (Qopp_le_compat 0). apply (Qpos_nonneg (e1+e2)). intros. intros. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), (Qpos_nonneg (e1+e2)). unfold Qminus. rewrite <- Qle_minus_iff. exact H0. intros. apply (Qle_trans _ (approximate ((1 # 2)%Q ↾ eq_refl * e1)%Qpos - approximate e2)). destruct regFun_prf as [H1 _]. refine (Qle_trans _ _ _ _ H1). simpl. ring_simplify. apply Qplus_le_l. apply Qmult_le_r. apply Qpos_ispos. discriminate. apply Qplus_le_r. apply Qopp_le_compat. apply Qmin_case. intros. exact H0. intros. apply Qle_refl. - apply Qmin_case. apply Qmin_case. intros. unfold Qminus. rewrite Qplus_opp_r. apply (Qpos_nonneg (e1+e2)). intros. apply (Qle_trans _ (approximate ((1 # 2) * e1)%Qpos - approximate e2)). apply Qplus_le_l, H0. destruct regFun_prf as [_ H1]. apply (Qle_trans _ _ _ H1). apply Qplus_le_l. simpl. rewrite <- (Qmult_1_l (proj1_sig e1)) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. intros. apply Qmin_case. intros. apply (Qle_trans _ 0). apply (Qplus_le_l _ _ a). ring_simplify. exact H. apply (Qpos_nonneg (e1+e2)). intros. destruct regFun_prf as [_ H1]. apply (Qle_trans _ _ _ H1). apply Qplus_le_l. simpl. rewrite <- (Qmult_1_l (proj1_sig e1)) at 2. 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