proposition: Lemma hook_length_prod_nat (p : intpart) : #|{:stdtabsh p}| * (hook_length_prod p) = (sumn p)`!.
proof: Proof. apply /eqP; rewrite -eqz_nat PoszM. rewrite -(@eqr_int rat) intrM /=. have /= -> := HookLengthFormula_rat p. apply/eqP; rewrite -mulrA -[RHS]mulr1; congr (_ * _)%R. rewrite mulrC divff // intr_eq0. by rewrite eqz_nat; apply: hook_length_prod_non0. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure