proposition: Lemma leq_bigmin f g n : (forall i, i <= n -> f i <= g i) -> \min_(i <= n) f i <= \min_(i <= n) g i.
proof: Proof. elim: n => /= [->//|n IH H]. rewrite leq_min !geq_min H //= orbC IH // => i iLn. by rewrite H // (leq_trans iLn). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)