proposition: Fact nat_sinc (f : nat -> nat) a b : (forall x, a <= x < b -> f x < f (S x)) -> (forall x y, a <= x < y /\ y <= b -> f x < f y).
proof: Proof. intros H1. assert (forall n m, n <= m <= b - a -> f (a+n) <= f (a+m)) as H2. intros n m (H2 & H3); revert H2 H3. induction 1 as [ | m Hm IH ]; auto. intros H. spec in IH. lia. apply Nat.le_trans with (1 := IH). replace (a+S m) with (S (a+m)) by lia. apply Nat.lt_le_incl, H1; lia. assert (forall n m, n < m <= b - a -> f (a+n) < f (a+m)) as H3. unfold lt at 1; intros n m H. specialize (H1 (a+n)). spec in H1. lia. apply Nat.lt_le_trans with (1 := H1). replace (S (a+n)) with (a+S n) by lia. apply H2; auto. intros x y H4. replace x with (a+(x-a)) by lia. replace y with (a+(y-a)) by lia. apply H3. lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)