proposition: Lemma leq_minn2r m n p : m <= n -> minn m p <= minn n p.
proof: Proof. move=> mLn; rewrite /minn. case: leqP => pLm; case: leqP => //. by rewrite ltnNge (leq_trans pLm). by move=> _; rewrite ltnW. Qed.
imports: mathcomp(all_ssreflect finmap)