proposition: Lemma size_hook_box_indices rc : size (hook_box_indices rc) = (hook_length p rc).-1.
proof: Proof. move: rc => [r c]; rewrite /= size_cat !size_map !size_iota. rewrite /hook_length /leg_length /arm_length /=. by rewrite -!subn1 -!subnDA !add1n !addn1 addnC. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure