proposition: Lemma hook_length_prod_div (p : intpart) : (hook_length_prod p) %| (sumn p)`!.
proof: Proof. by apply/dvdnP; exists #|{:stdtabsh p}|; rewrite hook_length_prod_nat. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure