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