proposition: Lemma Max_seq_char : forall n, [0] [<] x[-]y and Max_seq n [=] x or x[-]y [<] one_div_succ n and Max_seq n [=] y.
proof: Proof. intros. unfold Max_seq in |- *. elim less_cotransitive_unfolded; intro H; simpl in |- *. left; split; algebra. right; split; algebra. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq