proposition: Fact inc_seq_split_lt n f k : (forall i j, i < j < n -> f i < f j) -> { p | p <= n /\ (forall i, i < p -> f i < k) /\ forall i, p <= i < n -> k <= f i }.
proof: Proof. revert f; induction n as [ | n IHn ]; intros f Hf. + exists 0; split; auto; split; intros; lia. + destruct (le_lt_dec k (f 0)) as [ H | H ]. - exists 0; split; try lia. split; intros i Hi; try lia. destruct i as [ | i ]; auto. apply Nat.le_trans with (1 := H), Nat.lt_le_incl, Hf; lia. - destruct (IHn (fun i => f (S i))) as (p & H1 & H2 & H3). * intros; apply Hf; lia. * exists (S p); split; try lia; split. ++ intros [ | i ] Hi; auto; apply H2; lia. ++ intros [ | i ] Hi; try lia; apply H3; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)