proposition: Lemma uneven_CRplus_is_RegularFunction: is_RegularFunction_noInf _ uneven_CRplus_approx.
proof: Proof. Proof with auto. intros e1 e2. unfold uneven_CRplus_approx. simpl. assert (QposEq (e1 + e2) ((e1 * ll + e2 * ll) + (e1 * rr + e2 * rr))). { unfold QposEq. transitivity (proj1_sig (e1 + e2)%Qpos * proj1_sig (ll + rr)%Qpos). unfold QposEq in llrr. rewrite llrr. simpl. ring. simpl. ring. } apply (ball_wd _ H _ _ (reflexivity _) _ _ (reflexivity _)). clear H. apply Qball_plus. apply (regFun_prf x (e1*ll)%Qpos (e2*ll)%Qpos). apply (regFun_prf y (e1*rr)%Qpos (e2*rr)%Qpos). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.reals.fast.CRArith