proposition: Lemma FSum_resp_less : forall (f g : nat -> PartIR) m n, m <= n -> (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 f g m n H H0 x HxF HxG. simpl in |- *. apply Sum_resp_less; try assumption. intros; apply H0; assumption. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality