proposition: Lemma growing_transit : forall {R : ConstructiveReals} (un : nat -> CRcarrier R), (forall n:nat, un n <= un (S n)) -> forall n p : nat, le n p -> un n <= un p.
proof: Proof. induction p. - intros. inversion H0. apply CRle_refl. - intros. apply Nat.le_succ_r in H0. destruct H0. apply (CRle_trans _ (un p)). apply IHp, H0. apply H. subst n. apply CRle_refl. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits