proposition: Lemma n_Function_ball01_plus : forall n e p1 p2 p3, (n_Function_ball01 n e (MVP_CR_apply n p2) (MVP_CR_apply n p3)) -> (n_Function_ball01 n e (MVP_CR_apply n (p1[+]p2)) (MVP_CR_apply n (p1[+]p3))).
proof: Proof. induction n; intros e p1 p2 p3 H. intros d1 d2. simpl. unfold Qball. unfold Cap_raw. simpl. replace RHS with ((approximate p1 ((1 # 2) * d1)%Qpos - approximate p1 ((1 # 2) * d2)%Qpos) +(approximate p2 ((1 # 2) * d1)%Qpos - approximate p3 ((1 # 2) * d2)%Qpos)) by simpl; ring. replace LHS with (((1 # 2) * proj1_sig d1 + (1 # 2) * proj1_sig d2)%Q +(proj1_sig ((1 # 2) * d1)%Qpos + e + proj1_sig ((1 # 2) * d2)%Qpos))%Q by simpl; ring. apply AbsSmall_plus. change (ball (proj1_sig ((1 # 2) * d1 + (1 # 2) * d2)%Qpos) (approximate p1 ((1 # 2) * d1)%Qpos) (approximate p1 ((1 # 2) * d2)%Qpos)). generalize ((1#2)*d1)%Qpos ((1#2)*d2)%Qpos. change (regFunEq p1 p1). apply regFunEq_equiv. reflexivity. generalize ((1#2)*d1)%Qpos ((1#2)*d2)%Qpos. apply H. intros x Hx0 Hx1. change (n_Function_ball01 n e (MVP_CR_apply _ (p1[+]p2) ! (MVP_C_ CRasCRing _ x)) (MVP_CR_apply _ (p1[+]p3) ! (MVP_C_ CRasCRing _ x))). eapply n_Function_ball01_wd;[| | |apply IHn]. reflexivity. apply Morphism_prf. apply plus_apply. apply Morphism_prf. apply plus_apply. apply: H; auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.algebra.Bernstein CoRN.algebra.CRing_Homomorphisms CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.model.totalorder.QMinMax CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.reals.fast.CRabs CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.CRArith CoRN.reals.fast.CRArith_alg CoRN.algebra.RSetoid