proposition: Lemma bigmin_leqP f n m : reflect (forall i, i <= n -> m <= f i) (m <= \min_(i <= n) f i).
proof: Proof. elim: n => /= [|n IH]. by apply: (iffP idP) => [mLf0 [|i] //|->]. apply: (iffP idP) => [|H]. rewrite leq_min => /andP[mLf mLmin] i. case: ltngtP => // [iLn _|-> _ //]. by rewrite ltnS in iLn; move: i iLn; apply/IH. rewrite leq_min H //=. by apply/IH => i iLn; rewrite H // (leq_trans iLn). Qed.
imports: mathcomp(all_ssreflect finmap)