proposition: Lemma FSum_wd' : forall m n, m <= S n -> forall f g : nat -> PartIR, (forall x HxF HxG i, m <= i -> i <= n -> 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'; try assumption. algebra. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality