proposition: Lemma subn_maxr : left_distributive subn maxn.
proof: Proof. move=> m n p; rewrite /maxn; case: leqP => [nLm|mLn]. by rewrite ltnNge leq_sub2r. have [nLp|pLn] := leqP n p; last by rewrite ltn_sub2r. apply/eqP; move: (nLp); rewrite -subn_eq0 => /eqP->. by rewrite ltnNge //= eq_sym subn_eq0 (leq_trans (ltnW mLn)). Qed.
imports: mathcomp(all_ssreflect finmap)