proposition: Lemma CR_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 Qabs ConstructiveReals ConstructiveAbs