proposition: Lemma interp_side_equa_in_N_R_compat : forall s l un, interp_side_equa_in_N s (map (@projT1 _ infinite_cv_radius) l) = Some un -> {f | interp_side_equa_in_R s l = Some f}.
proof: Proof. intro s ; induction s ; intros l un H. exists (fun _ => r) ; reflexivity. simpl in * ; destruct (interp_side_equa_in_N s (map (@projT1 _ infinite_cv_radius) l)) eqn: Heqb. specialize (IHs l r0 Heqb); destruct IHs as [f Hf] ; exists ((fun _ => r) * f)%F ; rewrite Hf ; reflexivity. inversion H. assert (Hrew := map_nth_error (@projT1 _ infinite_cv_radius) p l) ; destruct (nth_error l p) eqn:Heqb. specialize (Hrew s (eq_refl (Some s))). destruct s as [An rAn] ; simpl in H, Hrew ; rewrite Hrew in H ; simpl in H ; exists (fun x => nth_derive (sum An rAn) (D_infty_Rpser An rAn k) (a * x)) ; simpl ; rewrite Heqb ; reflexivity. simpl in H. assert (T := map_nth_error2 (@projT1 _ infinite_cv_radius) _ _ Heqb). rewrite T in H ; inversion H. simpl in * ; destruct (interp_side_equa_in_N s (map (@projT1 _ infinite_cv_radius) l)) eqn:Heqb. specialize (IHs l r Heqb); destruct IHs as [f Hf]. exists (- f)%F ; rewrite Hf ; reflexivity. inversion H. simpl in *. 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. specialize (IHs1 l r Heqb); destruct IHs1 as [f Hf] ; specialize (IHs2 l r0 Heqb0); destruct IHs2 as [g Hg]. exists (f - g)%F ; rewrite Hf, Hg ; reflexivity. inversion H. inversion H. simpl in *. 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. specialize (IHs1 l r Heqb); destruct IHs1 as [f Hf] ; specialize (IHs2 l r0 Heqb0); destruct IHs2 as [g Hg]. exists (f + g)%F ; rewrite Hf, Hg ; reflexivity. inversion H. inversion H. simpl in *. 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. specialize (IHs1 l r Heqb); destruct IHs1 as [f Hf] ; specialize (IHs2 l r0 Heqb0); destruct IHs2 as [g Hg]. exists (f * g)%F ; rewrite Hf, Hg ; reflexivity. inversion H. inversion H. 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