proposition: Lemma Taylor_Sumx_lemma : forall n x z y y', (forall H, y 0 H [=] z) -> (forall i H H', y' i H' [=] y (S i) H) -> x[-]Sumx (G:=IR) (n:=S n) y [=] x[-]z[-]Sumx (G:=IR) (n:=n) y'.
proof: Proof. intro; induction n as [| n Hrecn]. intros; simpl in |- *. astepl (x[-] ([0][+]z)). rational. intros. astepl (x[-] (Sumx (fun i (l : i < S n) => y i (Nat.lt_lt_succ_r _ _ l)) [+] y (S n) (Nat.lt_succ_diag_r (S n)))). rstepl (x[-]Sumx (fun i (l : i < S n) => y i (Nat.lt_lt_succ_r _ _ l)) [-] y (S n) (Nat.lt_succ_diag_r (S n))). astepr (x[-]z[-] (Sumx (fun i (l : i < n) => y' i (Nat.lt_lt_succ_r _ _ l)) [+]y' n (Nat.lt_succ_diag_r n))). rstepr (x[-]z[-]Sumx (fun i (l : i < n) => y' i (Nat.lt_lt_succ_r _ _ l)) [-] y' n (Nat.lt_succ_diag_r n)). algebra. Qed.
imports: CoRN.ftc.TaylorLemma