proposition: Lemma lft_leEq_MAX : x [<=] MAX.
proof: Proof. astepr ([0][+]MAX); apply shift_leEq_plus. apply approach_zero_weak. intros e He. apply leEq_wdl with (Lim (Cauchy_const x) [-]MAX). 2: apply cg_minus_wd; [ apply eq_symmetric_unfolded; apply Lim_const | algebra ]. unfold MAX in |- *. eapply leEq_wdl. 2: apply Lim_minus. simpl in |- *. elim (Archimedes ([1][/] e[//]pos_ap_zero _ _ He)); intros n Hn. cut ([0] [<] nring (R:=IR) n). intro posn. apply str_seq_leEq_so_Lim_leEq. exists n; intros i Hi. simpl in |- *. unfold Max_seq in |- *. elim less_cotransitive_unfolded; intro H; simpl in |- *. astepl ZeroR; apply less_leEq; auto. apply less_leEq; eapply less_transitive_unfolded. apply H. unfold one_div_succ, Snring in |- *; apply shift_div_less. apply pos_nring_S. apply shift_less_mult' with (pos_ap_zero _ _ He). auto. eapply leEq_less_trans. apply Hn. apply nring_less; auto with arith. eapply less_leEq_trans. 2: apply Hn. apply recip_resp_pos; auto. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq