proposition: Lemma Sum_pres_less : forall s t : nat -> IR, (forall i, s i [<] t i) -> forall N m, N <= m -> Sum N m s [<=] Sum N m t.
proof: Proof. intros. apply less_leEq. apply Sum_resp_less; auto. Qed.
imports: CoRN.reals.CReals1