proposition: Lemma hook_boxes_empty rc : in_shape p rc -> hook_boxes rc = [::] -> corner_box p rc.
proof: Proof. Proof using. move=> Hpart Hhl. apply hook_length1_corner => //. suff -> : hook_length p rc = (size (hook_boxes rc)).+1 by rewrite Hhl. by rewrite size_map size_hook_box_indices. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure