proposition: Lemma FSum0_S : forall P f n, (forall m, included P (Dom (f m))) -> Feq P (FSum0 n f{+}f n) (FSum0 (S n) f).
proof: Proof. intros P f n H. FEQ. apply included_FPlus; auto. simpl in |- *; red in |- *; intros. apply (H n0); auto. simpl in |- *. red in |- *; intros; apply (H n0); auto. simpl in |- *; apply bin_op_wd_unfolded; algebra. apply Sum0_wd; algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality