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