proposition: Lemma hook_length_prod_non0 (p : intpart) : (hook_length_prod p) != 0.
proof: Proof. rewrite /hook_length_prod -eqz_nat !(big_morph Posz PoszM (id1 := Posz 1%N)) //. by apply/prodf_neq0 => [] [] [r c]. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure