proposition: Lemma coeffXdiff (b : 'I_n) (k : 'X_{1..n}) (i : 'I_n) : (k <= rbound b)%MM -> ('X_i - 'X_b)@_k = (k == U_(i)%MM)%:R.
proof: Proof. Proof using. rewrite mcoeffB !mcoeffX => Hk. suff -> : (U_(b)%MM == k) = false by rewrite subr0 eq_sym. apply/negP => /eqP; rewrite mnmP => /(_ b). rewrite mnm1E eq_refl => /esym /= => Hkb. have {Hkb} : k b != 0%N by rewrite Hkb. by rewrite -lep1mP => /lepm_trans/(_ Hk); rewrite lep1mP mnmE /= subnn eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition