proposition: Lemma selectOneInSum : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n i : nat), le i n -> (forall k:nat, 0 <= u k) -> u i <= CRsum u n.
proof: Proof. induction n. - intros. inversion H. subst i. apply CRle_refl. - intros. apply Nat.le_succ_r in H. destruct H. + apply (CRle_trans _ (CRsum u n)). * apply IHn. -- assumption. -- assumption. * simpl. apply Rplus_le_pos. apply H0. + subst i. simpl. rewrite CRplus_comm. apply Rplus_le_pos. apply cond_pos_sum. intros. apply H0. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits