proposition: Lemma less_MAX_imp : forall z : IR, z [<] MAX -> z [<] x or z [<] y.
proof: Proof. intros z H. unfold MAX in H. elim (less_Lim_so_less_seq _ _ H). intros N HN. simpl in HN. elim (Max_seq_char N); intro Hseq; inversion_clear Hseq; [ left | right ]; astepr (Max_seq N); auto with arith. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq