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