proposition: Lemma find_minn_bound (p : pred nat) m : {n | [/\ n < m, p n & forall i, i < n -> ~~ p i]} + {(forall i, i < m -> ~~ p i)}.
proof: Proof. case: (boolP [exists n : 'I_m, p n]) => C ; [left|right]. - have/find_ex_minn: exists n, (n < m) && p n. case/existsP : C => [[n Hn pn]] /=. exists n. by rewrite Hn. case => n /andP [lt_m pn] min_n. exists n. split => // i Hi. apply: contraTN (Hi) => pi. rewrite -leqNgt min_n // pi andbT. exact: ltn_trans lt_m. - move => i lt_m. move: C. by rewrite negb_exists => /forallP /(_ (Ordinal lt_m)). Qed.
imports: mathcomp(all_ssreflect)