proposition: Theorem CS_seq_bounded : forall g : nat -> R, Cauchy_prop g -> {K : R | [0] [<] K | {N : nat | forall m, N <= m -> AbsSmall K (g m)}}.
proof: Proof. intros g Hg. unfold Cauchy_prop in |- *. elim (Hg _ (pos_one _)). intros N H1. exists (g N[^]2[-]g N[+]Two). apply less_leEq_trans with (nring (R:=R) 7 [/]FourNZ). apply pos_div_four; apply nring_pos; auto with arith. astepl ([0][+]nring (R:=R) 7 [/]FourNZ). apply shift_plus_leEq. rstepr ((g N[-][1] [/]TwoNZ)[^]2). apply sqr_nonneg. exists N. intros m Hm. elim (H1 m Hm); intros. split. apply plus_cancel_leEq_rht with (z := [--](g N)). rstepr (g m[-]g N). rstepl ([--](g N[^]2[+]Two)). apply leEq_transitive with ([--]([1]:R)). apply inv_cancel_leEq. rstepl ([1]:R). rstepr (g N[^]2[+]Two). apply plus_cancel_leEq_rht with ([--][1]:R). rstepl ([0]:R). rstepr (g N[^]2[+][1]). apply leEq_transitive with (y := g N[^]2). apply sqr_nonneg. apply less_leEq; apply less_plusOne. assumption. apply plus_cancel_leEq_rht with (g N[-]Two). rstepr (g N[^]2). astepr (g N[*]g N). apply plus_cancel_leEq_rht with ([--](Two[*]g N)[+]Two). rstepl (g m[-]g N). rstepr (g N[*]g N[+][1][-]Two[*]g N[+][1]). apply leEq_transitive with (y := [1]:R). assumption. rstepl ([0][+]([1]:R)). apply plus_resp_leEq with (z := [1]:R). rstepr ((g N[-][1])[*](g N[-][1])). apply leEq_wdr with (y := (g N[-][1])[^]2). apply sqr_nonneg. algebra. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)