proposition: Lemma zero_less_AbsIR_plus_one : forall q : IR, [0] [<] AbsIR q[+][1].
proof: Proof. intros. apply less_leEq_trans with ([0][+]OneR). rstepr OneR; apply pos_one. apply plus_resp_leEq; apply AbsIR_nonneg. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq