proposition: Lemma FSum_0 : forall P f n, (forall i, included P (Dom (f i))) -> Feq P (f n) (FSum n n f).
proof: Proof. intros P f n H. FEQ. simpl in |- *. red in |- *; intros; apply (H n0); auto. simpl in |- *. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. apply Sum_one. algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality