proposition: Lemma inv_FSum : forall (f : nat -> PartIR) m n x Hx Hx', FSum m n (fun i => {--} (f i)) x Hx [=] [--] (FSum m n f x Hx').
proof: Proof. intros. simpl in |- *. eapply eq_transitive_unfolded. 2: apply inv_Sum. apply Sum_wd; intros; rational. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality