proposition: Lemma FSum_wd : forall m n (f g : nat -> PartIR), (forall x HxF HxG i, f i x (HxF i) [=] g i x (HxG i)) -> forall x HxF HxG, FSum m n f x HxF [=] FSum m n g x HxG.
proof: Proof. intros. simpl in |- *. apply Sum_wd. algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality