proposition: Lemma polyX_inj (i j : 'I_n) : 'X_i = 'X_j -> i = j.
proof: Proof. Proof using. move/(congr1 (mcoeff U_(j))); rewrite !mcoeffX eq_refl /=. case: (_ =P _) => [H _ | _ /esym /= /eqP] /=. - have:= congr1 (fun x : 'X_{1..n} => x j) H. by rewrite !mnm1E eq_refl eq_sym; case: eqP. - by have:= oner_neq0 R => /negbTE ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition