proposition: Lemma less_AbsIR : forall x y, [0] [<] x -> x [<] AbsIR y -> x [<] y or y [<] [--]x.
proof: Proof. intros x y H H0. simpl in H0. unfold ABSIR in H0. cut (x [<] y or x [<] [--]y). intro H1; inversion_clear H1. left; assumption. right; astepl ( [--][--]y); apply inv_resp_less; assumption. apply less_Max_imp; assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq