proposition: Lemma Sin_plus_fun : forall y : IR, Feq realline (F y) (G y).
proof: Proof. intro. cut (Taylor_bnd (F' y)). intro H. cut (Taylor_bnd (G' y)). intro H0. cut (forall n : nat, Continuous realline (G' y n)). intro H1; apply Taylor_unique_crit with ZeroR (F' y) (G' y) (Sin_plus_der_lft y) H. exact (Sin_plus_der_rht y). auto. apply Sin_plus_eq. apply Taylor_Series_conv_to_fun. auto. apply four_induction with (P := fun n : nat => Continuous realline (G' y n)). simpl in |- *; Contin. simpl in |- *; Contin. simpl in |- *; Contin. simpl in |- *; Contin. auto. apply Sin_plus_Taylor_bnd_rht. apply Sin_plus_Taylor_bnd_lft. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)