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