proposition: Lemma Vanprod_coeff_rho : Delta@_rho = 1.
proof: Proof. Proof using. rewrite /Vanprod. case: (n =P 0%N) => [Hn | /eqP]. - rewrite big1; last by move=> [[i Hi]]; exfalso; rewrite Hn in Hi. suff -> : rho = 0%MM by rewrite mcoeff1 eq_refl. by rewrite mnmP => [[i Hi]]; exfalso; rewrite Hn in Hi. - rewrite -lt0n => /prednK/eqP; rewrite eqn_leq => /andP[]. move=> /mcoeff_arbound <- _. rewrite /rho subn1; congr mcoeff. apply eq_bigl => [[i j]] /=. case: n i j => [//=| n'] i j /=; first by exfalso; have:= ltn_ord i. by rewrite -(ltnS j) ltn_ord andbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition