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