proposition: Lemma card_stpn_shape_hook : #|[set p : stpn | shape p.1 == shape p.2]| = \sum_(sh : 'P_n) (n`! %/ (hook_length_prod sh))^2.
proof: Proof. Proof using. rewrite card_stpn_shape; apply eq_bigr => sh _; congr (_ ^ 2). by rewrite HookLengthFormula sumn_intpartn. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype choice ssrnat seq ssrint div rat fintype finset bigop path ssralg ssrnum order) ordtype partition tableau Schensted std stdtab hook