proposition: Lemma intcompn_cons_sub_proof i n (c : intcompn (n - i)) : i != 0%N -> i <= n -> is_comp_of_n n (i :: c).
proof: Proof. move=> Hi Hin. rewrite /is_comp_of_n /= intcompn_sumn subnKC // eq_refl /=. rewrite /is_comp inE negb_or eq_sym Hi /=. exact: intcompnP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv