proposition: Lemma interp_side_equa_in_N_R : forall s l Un f, interp_side_equa_in_N s (map (@projT1 _ infinite_cv_radius) l) = Some Un -> interp_side_equa_in_R s l = Some f -> {pr : infinite_cv_radius Un | sum Un pr == f}.
proof: Proof. intro s ; induction s ; simpl ; intros l Un f HN HR3. inversion HN ; inversion HR3 ; subst ; exists (constant_infinite_cv_radius r) ; apply constant_is_cst. destruct (interp_side_equa_in_N s (map (@projT1 _ infinite_cv_radius) l)) eqn:Heqb. destruct (interp_side_equa_in_R s l) eqn:Heqb0. specialize (IHs l r0 r1 Heqb Heqb0). inversion HR3 as [Hrew] ; destruct Hrew. inversion HN as [Hrew] ; destruct Hrew. destruct IHs as [rho Hrho]. assert (pr : infinite_cv_radius (r * r0)). destruct (Req_dec r 0) as [Heq | Hneq]. rewrite Heq ; simpl ; rewrite <- (infinite_cv_radius_ext (Rseq_constant 0)) ; [apply zero_infinite_cv_radius | intro n ; unfold Rseq_mult ; rewrite Rmult_0_l ; reflexivity]. rewrite <- infinite_cv_radius_scal_compat ; assumption. exists pr ; intro x ; unfold mult_fct ; rewrite <- Hrho. apply sum_scal_compat. inversion HR3. inversion HN. assert (Hrew := map_nth_error (@projT1 _ infinite_cv_radius) p l) ; unfold Bind in * ; destruct (nth_error l p). specialize (Hrew s (eq_refl (Some s))); destruct s as [An rAn] ; rewrite Hrew in HN ; inversion HN as [HN0] ; destruct HN0 ; inversion HR3 as [HR30] ; destruct HR30. assert (ppr: infinite_cv_radius (An_nth_deriv An k)). rewrite <- infinite_cv_radius_nth_derivable_compat ; assumption. assert (pr : infinite_cv_radius (An_expand (An_nth_deriv An k) a)). apply infinite_cv_radius_expand_compat ; assumption. exists pr ; intro x ; symmetry ; rewrite (sum_expand_compat _ ppr). erewrite <- nth_derive_sum_explicit ; reflexivity. inversion HR3. destruct (interp_side_equa_in_N s (map (@projT1 _ infinite_cv_radius) l)) eqn:Heqb. destruct (interp_side_equa_in_R s l) eqn:Heqb0. specialize (IHs l r r0 Heqb Heqb0). inversion HR3 as [Hrew] ; destruct Hrew. inversion HN as [Hrew] ; destruct Hrew. destruct IHs as [rho Hrho]. assert (pr : infinite_cv_radius (- r)) by (rewrite <- infinite_cv_radius_opp_compat ; assumption). exists pr ; intro x ; unfold opp_fct ; rewrite <- Hrho ; apply sum_opp_compat. inversion HR3. inversion HN. destruct (interp_side_equa_in_N s1 (map (@projT1 _ infinite_cv_radius) l)) eqn:Heqb. destruct (interp_side_equa_in_N s2 (map (@projT1 _ infinite_cv_radius) l)) eqn:Heqb0. destruct (interp_side_equa_in_R s1 l) eqn:Heqb1. destruct (interp_side_equa_in_R s2 l) eqn:Heqb2. inversion HN as [Hrew] ; destruct Hrew ; inversion HR3 as [Hrew] ; destruct Hrew. specialize (IHs1 l r r1 Heqb Heqb1); specialize (IHs2 l r0 r2 Heqb0 Heqb2). destruct IHs1 as [rho1 Hrho1] ; destruct IHs2 as [rho2 Hrho2]. assert (pr : infinite_cv_radius (r - r0)). apply infinite_cv_radius_minus_compat ; assumption. exists pr. intro x ; unfold minus_fct ; rewrite <- Hrho1, <- Hrho2 ; apply sum_minus_compat. inversion HR3. inversion HR3. inversion HN. inversion HN. destruct (interp_side_equa_in_N s1 (map (@projT1 _ infinite_cv_radius) l)) eqn:Heqb. destruct (interp_side_equa_in_N s2 (map (@projT1 _ infinite_cv_radius) l)) eqn:Heqb0. destruct (interp_side_equa_in_R s1 l) eqn:Heqb1. destruct (interp_side_equa_in_R s2 l) eqn:Heqb2. inversion HN as [Hrew] ; destruct Hrew ; inversion HR3 as [Hrew] ; destruct Hrew. specialize (IHs1 l r r1 Heqb Heqb1); specialize (IHs2 l r0 r2 Heqb0 Heqb2). destruct IHs1 as [rho1 Hrho1] ; destruct IHs2 as [rho2 Hrho2]. assert (pr : infinite_cv_radius (r + r0)). apply infinite_cv_radius_plus_compat ; assumption. exists pr. intro x ; unfold plus_fct ; rewrite <- Hrho1, <- Hrho2 ; apply sum_plus_compat. inversion HR3. inversion HR3. inversion HN. inversion HN. destruct (interp_side_equa_in_N s1 (map (@projT1 _ infinite_cv_radius) l)) eqn:Heqb. destruct (interp_side_equa_in_N s2 (map (@projT1 _ infinite_cv_radius) l)) eqn:Heqb0. destruct (interp_side_equa_in_R s1 l) eqn:Heqb1. destruct (interp_side_equa_in_R s2 l) eqn:Heqb2. inversion HN as [Hrew] ; destruct Hrew ; inversion HR3 as [Hrew] ; destruct Hrew. specialize (IHs1 l r r1 Heqb Heqb1); specialize (IHs2 l r0 r2 Heqb0 Heqb2). destruct IHs1 as [rho1 Hrho1] ; destruct IHs2 as [rho2 Hrho2]. assert (pr : infinite_cv_radius (r # r0)). apply infinite_cv_radius_prod_compat ; assumption. exists pr. intro x ; unfold mult_fct ; rewrite <- Hrho1, <- Hrho2 ; apply sum_mult_compat. inversion HR3. inversion HR3. inversion HN. inversion HN. Qed.
imports: Rsequence_def Rsequence_sums_facts Rpser Rfunction_facts Rextensionality Rfunction_classes Nth_derivative_def Nth_derivative_facts Dequa_def List PeanoNat Tactics Option