proposition: Lemma alt_rho_non0 : 'a_rho != 0.
proof: Proof. Proof using . exact: alt_uniq_non0 (rho_uniq _). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition mathcomp(matrix)