proposition: Theorem HookLengthFormula (p : intpart) : #|{:stdtabsh p}| = (sumn p)`! %/ (hook_length_prod p).
proof: Proof. by rewrite -hook_length_prod_nat mulnK // lt0n; exact: hook_length_prod_non0. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure