proposition: Lemma Sin_plus_eq : forall y n HaF HaG, F' y n [0] HaF [=] G' y n [0] HaG.
proof: Proof. do 2 intro; apply four_ind with (P := fun n : nat => forall HaF HaG, F' y n [0] HaF [=] G' y n [0] HaG). intros; simpl in |- *. apply eq_transitive_unfolded with (Sin y). simpl in |- *; rational. apply eq_transitive_unfolded with (Sin [0][*]Cos y[+]Cos [0][*]Sin y). 2: simpl in |- *; algebra. rstepl ([0][*]Cos y[+][1][*]Sin y). algebra. intros; simpl in |- *. apply eq_transitive_unfolded with (Cos y). simpl in |- *; rational. apply eq_transitive_unfolded with (Cos [0][*]Cos y[-]Sin [0][*]Sin y). 2: simpl in |- *; algebra. rstepl ([1][*]Cos y[-][0][*]Sin y). algebra. intros; simpl in |- *. apply un_op_wd_unfolded. apply eq_transitive_unfolded with (Sin y). simpl in |- *; rational. apply eq_transitive_unfolded with (Sin [0][*]Cos y[+]Cos [0][*]Sin y). 2: simpl in |- *; algebra. rstepl ([0][*]Cos y[+][1][*]Sin y). algebra. intros; simpl in |- *. apply eq_transitive_unfolded with ( [--] (Cos y)). simpl in |- *; rational. apply eq_transitive_unfolded with (Sin [0][*]Sin y[-]Cos [0][*]Cos y). 2: simpl in |- *; algebra. rstepl ([0][*]Sin y[-][1][*]Cos y). algebra. intros. simpl in |- *; auto. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)