proposition: Lemma eq_bigmin f n : {i0 : 'I_n.+1 | \min_(i <= n) f i = f i0}.
proof: Proof. elim: n => /= [|n [i ->]]; first by exists ord0. rewrite /minn; case: leqP => H. by exists (inord i); rewrite inordK // (leq_trans (ltn_ord i)). by exists ord_max. Qed.
imports: mathcomp(all_ssreflect finmap)