proposition: Lemma FSum_one : forall n (f : nat -> PartIR) x Hx Hx', FSum n n f x Hx' [=] f n x Hx.
proof: Proof. intros. simpl in |- *. eapply eq_transitive_unfolded. apply Sum_one. simpl in |- *; rational. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality