proposition: Lemma interp_equa_in_N_R : forall (e : diff_equa) (l : list (sigT infinite_cv_radius)), [| e |]N (map (@projT1 _ infinite_cv_radius) l) -> [| e |]R l.
proof: Proof. intros [s1 s2] l 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. destruct (interp_side_equa_in_R s1 l) eqn:Heqb1. destruct (interp_side_equa_in_R s2 l) eqn:Heqb2. destruct (interp_side_equa_in_N_R s1 l r r1 Heqb Heqb1) as [rho1 Hrho1]. destruct (interp_side_equa_in_N_R s2 l r0 r2 Heqb0 Heqb2) as [rho2 Hrho2]. rewrite <- Hrho1, <- Hrho2 ; apply sum_ext ; assumption. destruct (interp_side_equa_in_N_R_compat _ _ _ Heqb0) as [f Hf] ; rewrite Hf in Heqb2 ; inversion Heqb2. destruct (interp_side_equa_in_N_R_compat _ _ _ Heqb) as [f Hf] ; rewrite Hf in Heqb1 ; inversion Heqb1. 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