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