proposition: Lemma bigmin_inf f n i0 m : i0 <= n -> f i0 <= m -> \min_(i <= n) f i <= m.
proof: Proof. move=> i0Ln fi0Lm; apply: leq_trans fi0Lm. elim: n i0Ln => /= [|n IH]; first by case: i0. by case: ltngtP => // [i0Ln _| -> _]; rewrite geq_min ?leqnn ?IH ?orbT. Qed.
imports: mathcomp(all_ssreflect finmap)