proposition: Lemma hook_length_ltr sh r c j : is_part sh -> r < j -> in_shape sh (j, c) -> hook_length sh (j, c) < hook_length sh (r, c).
proof: Proof. rewrite /hook_length ltnS => Hpart Hr Hc. rewrite -addnS; apply leq_add. exact: arm_length_ler. exact: leg_length_ltr. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure