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