proposition: Lemma Vanprod_dhomog : Delta \is 'C(n, 2).-homog.
proof: Proof. Proof using. have /homogP[d Hd] : Delta \is homog [measure of mdeg]. rewrite /Vanprod -big_filter -(big_map _ xpredT id). apply homog_prod; apply/allP => X /mapP[[i j]/= _ ->{X}]. by apply/homogP; exists 1%N; apply rpredB; rewrite dhomogX /= mdeg1. suff <- : d = 'C(n, 2) by []. have Hr : rho \in msupp Delta. by rewrite mcoeff_msupp Vanprod_coeff_rho oner_neq0. move: Hd => /dhomogP/(_ _ Hr) /= <-. exact: mdeg_rho. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition