proposition: Fact inc_seq_split_le n f h : (forall i j, i < j < n -> f i < f j) -> { q | q <= n /\ (forall i, i < q -> f i <= h) /\ (forall i, q <= i < n -> h < f i) }.
proof: Proof. intros Hf. destruct inc_seq_split_lt with (1 := Hf) (k := S h) as (q & H1 & H2 & H3); exists q; split; auto; split. + intros i Hi; specialize (H2 _ Hi); lia. + intros i Hi; specialize (H3 _ Hi); lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)