proposition: Lemma basis_cover n d (m : 'X_{1..n}): (mdeg m == d) = (m \in sbasis n d).
proof: Proof. apply/eqP/idP=> [eq_szm_d|]. apply/mapP; have /eqP := size_m2s m; rewrite -eq_szm_d => sz_tm. exists (Tuple sz_tm); first by rewrite mem_enum inE /= srt_m2s. by rewrite s2mK. case/mapP=> /= t _ ->; pose F i := count_mem i t. rewrite mdegE (eq_bigr F) {}/F; last first. by move=> /= i _; rewrite mnmE. transitivity (\sum_i \sum_(j <- t | j == i) 1)%N. by apply: eq_bigr => i _; rewrite -big_filter sum1_size size_filter. rewrite (exchange_big_dep predT)//=. transitivity (\sum_(j <- t) 1)%N; last by rewrite sum1_size size_tuple. by apply: eq_bigr => i _; rewrite (eq_bigl _ _ (eq_sym _)) big_pred1_eq. 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