proposition: Lemma intcompn_behead_sub_proof i n (c : intcompn n) : i != 0%N -> i <= n -> is_comp_of_n (n - i)%N (if head 0%N c == i then behead c else rowcompn (n-i)).
proof: Proof. case: c => [[|c0 c] /= /andP[/eqP <- Hcomp]] Hi0 Hin. by exfalso; move: Hin Hi0; rewrite leqn0 => /eqP ->; rewrite eq_refl. case: (c0 =P i) => Hc0 /=; last exact: rowcompnP. subst c0; rewrite addKn eq_refl /=. move: Hcomp; rewrite /is_comp inE; apply contra => ->. by rewrite orbT. 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