proposition: Lemma estimate_abs : forall x : R, {X : R | [0] [<] X | AbsSmall X x}.
proof: Proof. intros. unfold AbsSmall in |- *. cut (x [<] x[+][1]). intro H. elim (less_cotransitive_unfolded _ x (x[+][1]) H [--]x); intro. exists ([--]x[+][1]). apply leEq_less_trans with ([--]x). 2: apply less_plusOne. apply less_leEq; apply mult_cancel_less with (Two:R). apply pos_two. astepl ([0]:R); rstepr ([--]x[-]x). apply shift_less_minus. astepl x; auto. split; apply less_leEq. astepr ([--][--]x). apply inv_resp_less. apply less_plusOne. apply less_transitive_unfolded with ([--]x). auto. apply less_plusOne. exists (x[+][1]). apply less_leEq_trans with (([1]:R) [/]TwoNZ). apply pos_div_two; apply pos_one. apply shift_leEq_plus; rstepl (([--][1]:R) [/]TwoNZ). apply shift_div_leEq. apply pos_two. rstepr (x[+]x); apply shift_leEq_plus. unfold cg_minus in |- *; apply shift_plus_leEq'. rstepr (x[+][1]); apply less_leEq; auto. split; apply less_leEq. astepr ([--][--]x). apply inv_resp_less. auto. auto. apply less_plusOne. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)