proposition: Lemma transition_le_gt (f: nat -> nat) (x n1 n2: nat): n1 <= n2 -> f n1 <= x -> x < f n2 -> exists n, n < n2 /\ f n <= x /\ x < f (1+n).
proof: Proof. move=> H Hfn1 Hfn2. have : n1 < n2. { suff : n1 <> n2 by lia. by move=> ?; subst; lia. } clear H. elim: n2 Hfn2; first by lia. move=> n2 IH ??. have [?|?] : f n2 <= x \/ x < f n2 by lia. - exists n2 => /=. lia. - have ? : n1 <> n2 by (move=> ?; subst; lia). have [n ?] := IH ltac:(lia) ltac:(lia). exists n. lia. Qed.
imports: Arith Lia ZArith.Znat ZArith.Zdiv ssreflect ssrbool ssrfun