proposition: Lemma bigmin_ext f1 f2 n : (forall i, i <= n -> f1 i = f2 i) -> \min_(i <= n) f1 i = \min_(i <= n) f2 i.
proof: Proof. elim: n => /= [->//|n IH H]. by rewrite H // IH // => i iH; rewrite H // (leq_trans iH). Qed.
imports: mathcomp(all_ssreflect finmap)