proposition: Lemma weird_mon_covers : forall n (f : nat -> nat), (forall i, f i < n -> f i < f (S i)) -> {m : nat | n <= f m | forall i, i < m -> f i < n}.
proof: Proof. intros; induction n as [| n Hrecn]. exists 0. auto with arith. intros; inversion H0. elim Hrecn. 2: auto. intros m Hm Hm'. elim (le_lt_eq_dec _ _ Hm); intro. exists m. assumption. auto with arith. exists (S m). apply Nat.le_lt_trans with (f m). rewrite b; auto with arith. apply H. rewrite b; apply Nat.lt_succ_diag_r. intros. elim (le_lt_eq_dec _ _ H0); intro. auto with arith. cut (i = m); [ intro | auto ]. rewrite b; rewrite <- H1. apply Nat.lt_succ_diag_r. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)