proposition: Lemma Sum0_pres_less : forall s t : nat -> IR, (forall i, s i [<] t i) -> forall n, Sum0 n s [<=] Sum0 n t.
proof: Proof. intros s t H. simple induction n. simpl in |- *. exact (leEq_reflexive _ _). intros. simpl in |- *. apply leEq_transitive with (Sum0 n0 t[+]s n0). apply plus_resp_leEq. assumption. apply plus_resp_leEq_lft. apply less_leEq; exact (H _). Qed.
imports: CoRN.reals.CReals1