proposition: Lemma CRplus_translate : forall (a:Q) (y:CR), (' a + y == translate a y)%CR.
proof: Proof. intros a y. unfold ucFun2, CRplus. unfold Cmap2. unfold inject_Q_CR. simpl. intros e1 e2. simpl. unfold Cap_raw. simpl. destruct y; simpl. simpl. split. - ring_simplify. destruct (regFun_prf ((1#2)*e1)%Qpos e2) as [H _]. simpl in H. refine (Qle_trans _ _ _ _ H). ring_simplify. apply Qplus_le_l. apply Qmult_le_r. apply Qpos_ispos. discriminate. - ring_simplify. destruct (regFun_prf ((1#2)*e1)%Qpos e2) as [_ H]. apply (Qle_trans _ _ _ H). apply Qplus_le_l. simpl. rewrite <- (Qmult_1_l (` 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