proposition: Lemma rht_leEq_MAX : y [<=] MAX.
proof: Proof. unfold MAX in |- *. apply leEq_seq_so_leEq_Lim. intro i; simpl in |- *. unfold Max_seq in |- *. elim less_cotransitive_unfolded; intro H; simpl in |- *. 2: apply leEq_reflexive. apply less_leEq; astepl ([0][+]y). apply shift_plus_less; auto. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq