proposition: Lemma maj_upto_eps : forall (F : COrdField) (a : nat -> F) (n : nat) (eps : F), 0 < n -> [0] [<] eps -> {k : nat | 1 <= k /\ k <= n /\ (forall i : nat, 1 <= i -> i <= n -> a i[-]eps [<=] a k)}.
proof: Proof. intros F a n eps Hn Heps. induction n as [| n Hrecn]. elim (Nat.lt_irrefl _ Hn). clear Hrecn Hn. induction n as [| n Hrecn]. exists 1. repeat split. 1-2: reflexivity. intros. rewrite <- (Nat.le_antisymm _ _ H H0). astepr (a 1[+][0]). unfold cg_minus in |- *. apply plus_resp_leEq_lft. astepr ([--]([0]:F)). apply less_leEq; apply inv_resp_less; auto. elim Hrecn; intros k Hk. cut (a (S (S n))[-]eps [<] a (S (S n))). intro H. elim (less_cotransitive_unfolded _ _ _ H (a k)); intro H4. exists k. elim Hk; intros H0 H2. elim H2; clear H2; intros H1 H2. repeat split. assumption. auto with arith. intros i H3 H5. elim (Cle_le_S_eq _ _ H5); intro H6. auto with arith. rewrite H6. apply less_leEq; assumption. exists (S (S n)). repeat split; auto with arith. intros i H0 H1. elim (Cle_le_S_eq _ _ H1); intro H2. apply leEq_transitive with (a k). elim Hk; intros H3 H5. elim H5; clear H5; intros H6 H7. auto with arith. apply less_leEq; assumption. rewrite H2; apply less_leEq; auto. rstepr (a (S (S n))[-][0]). apply minus_resp_less_rht. assumption. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)