proposition: Lemma mon_fun_covers : (forall i j, i < j -> h i < h j) -> h 0 = 0 -> forall n, {k : nat | S n <= h k} -> {i : nat | h i <= n | S n <= h (S i)}.
proof: Proof. intros H H0 n H1. elim H1; intros k Hk. induction k as [| k Hreck]. exists 0. rewrite H0; auto with arith. cut (h 0 < h 1); [ intro; apply Nat.le_trans with (h 0); auto with arith | apply H; apply Nat.lt_succ_diag_r ]. cut (h k < h (S k)); [ intro H2 | apply H; apply Nat.lt_succ_diag_r ]. elim (le_lt_dec (S n) (h k)); intro H3. elim (Hreck H3); intros i Hi. exists i; assumption. exists k; auto with arith. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)