proposition: Theorem HookLengthFormula_rat (p : intpart) : ( (#|{:stdtabsh p}|)%:Q = HLF p )%R.
proof: Proof. apply esym; move: p; apply card_stdtabsh_rat_rec. - by rewrite /= /hook_length_prod /= big_box_skew /= big_nil factE. - move=> p Hp; apply esym. exact: Corollary4_eq. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure