proposition: Lemma Sin_plus_Taylor_bnd_rht : forall y : IR, Taylor_bnd (G' y).
proof: Proof. clear F G F'; intros. apply bnd_imp_Taylor_bnd with (FAbs (Sine{*} [-C-] (Cos y) {+}Cosine{*} [-C-] (Sin y)) {+} FAbs (Cosine{*} [-C-] (Cos y) {-}Sine{*} [-C-] (Sin y))). intro; apply four_ind with (P := fun n : nat => forall (x : IR) Hx Hx', AbsIR (G' y n x Hx) [<=] AbsIR ((FAbs (Sine{*} [-C-] (Cos y) {+}Cosine{*} [-C-] (Sin y)) {+} FAbs (Cosine{*} [-C-] (Cos y) {-}Sine{*} [-C-] (Sin y))) x Hx')). intros. unfold G' in |- *. Opaque FAbs. simpl in |- *. eapply leEq_transitive. 2: apply leEq_AbsIR. astepl (AbsIR (Sine x (ProjIR1 (ProjIR1 Hx)) [*]Cos y[+] Cosine x (ProjIR1 (ProjIR2 Hx)) [*]Sin y) [+][0]). apply plus_resp_leEq_both. apply eq_imp_leEq; apply eq_symmetric_unfolded. Transparent FAbs. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 (ProjIR1 Hx')))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; rational. apply FAbs_nonneg. intros. unfold G' in |- *. Opaque FAbs. simpl in |- *. eapply leEq_transitive. 2: apply leEq_AbsIR. astepl ([0][+] AbsIR (Cosine x (ProjIR1 (ProjIR1 Hx)) [*]Cos y[-] Sine x (ProjIR1 (ProjIR2 Hx)) [*]Sin y)). apply plus_resp_leEq_both. apply FAbs_nonneg. apply eq_imp_leEq; apply eq_symmetric_unfolded. Transparent FAbs. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 (ProjIR2 Hx')))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; rational. intros. unfold G' in |- *. Opaque FAbs. simpl in |- *. eapply leEq_transitive. 2: apply leEq_AbsIR. astepl (AbsIR [--] (Sine x (ProjIR1 (ProjIR1 Hx)) [*]Cos y[+] Cosine x (ProjIR1 (ProjIR2 Hx)) [*]Sin y) [+][0]). apply leEq_wdl with (AbsIR (Sine x (ProjIR1 (ProjIR1 Hx)) [*]Cos y[+] Cosine x (ProjIR1 (ProjIR2 Hx)) [*]Sin y) [+][0]). apply plus_resp_leEq_both. apply eq_imp_leEq; apply eq_symmetric_unfolded. Transparent FAbs. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 (ProjIR1 Hx')))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; rational. apply FAbs_nonneg. apply bin_op_wd_unfolded. apply AbsIR_inv. algebra. intros. unfold G' in |- *. Opaque FAbs. simpl in |- *. eapply leEq_transitive. 2: apply leEq_AbsIR. astepl ([0][+] AbsIR (Sine x (ProjIR1 (ProjIR1 Hx)) [*]Sin y[-] Cosine x (ProjIR1 (ProjIR2 Hx)) [*]Cos y)). apply leEq_wdl with ([0][+] AbsIR (Cosine x (ProjIR1 (ProjIR2 Hx)) [*]Cos y[-] Sine x (ProjIR1 (ProjIR1 Hx)) [*]Sin y)). apply plus_resp_leEq_both. apply FAbs_nonneg. apply eq_imp_leEq; apply eq_symmetric_unfolded. Transparent FAbs. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 (ProjIR2 Hx')))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; rational. apply bin_op_wd_unfolded. algebra. apply AbsIR_minus. auto. Contin. apply four_induction with (P := fun n : nat => included (fun _ : IR => True) (Dom (G' y n))); auto; unfold G' in |- *. apply included_FPlus; Included. apply included_FMinus; Included. apply included_FInv; apply included_FPlus; Included. apply included_FMinus; Included. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)