proposition: Lemma bmnm_enumP : Finite.axiom bmnm_enum.
proof: Proof. case=> m lt_dm_b /=; rewrite count_uniq_mem; last first. rewrite (pmap_uniq (@insubK _ _ _)) 1?map_inj_uniq ?enum_uniq //. by move=> t1 t2 [] /(inj_map val_inj) /val_inj ->. apply/eqP; rewrite eqb1 mem_pmap_sub /=; apply/mapP. case: b m lt_dm_b=> // b' [m] /= lt_dm_Sb; exists [tuple of map inord m]. by rewrite mem_enum. apply/mnmP=> i; rewrite !multinomE !tnth_map inordK //. move: lt_dm_Sb; rewrite mdegE (bigD1 i) //= multinomE. by move=> /(leq_trans _) ->//; rewrite ltnS leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg