proposition: Lemma Cauchy_Max_seq : Cauchy_prop Max_seq.
proof: Proof. apply Cauchy_prop1_prop. intro k. exists k; intros m H. unfold Max_seq in |- *. elim less_cotransitive_unfolded; intro Hm; simpl in |- *; elim less_cotransitive_unfolded; intro Hk; simpl in |- *. astepr ZeroR; split; apply less_leEq. astepr ( [--]ZeroR); apply inv_resp_less; apply one_div_succ_pos. apply one_div_succ_pos. apply leEq_imp_AbsSmall; apply less_leEq; auto. apply AbsSmall_minus. apply leEq_imp_AbsSmall; apply less_leEq; auto. apply less_leEq_trans with (one_div_succ (R:=IR) m); auto. apply one_div_succ_resp_leEq; auto. astepr ZeroR; split; apply less_leEq. astepr ( [--]ZeroR); apply inv_resp_less; apply one_div_succ_pos. apply one_div_succ_pos. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq