proposition: Lemma insert_series_sum_char : forall n x Hx Hx', fun_seq_part_sum f n x Hx [=] fun_seq_part_sum insert_series (S n) x Hx'.
proof: Proof. intro; induction n as [| n Hrecn]. intros; simpl in |- *; algebra. intros; simpl in |- *; simpl in Hrecn; algebra. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions