proposition: Lemma walk_to_corner_end_simpl m r c : size (hook_box_indices (r, c)) = 0 -> walk_to_corner m (r, c) = Munit ([:: r], [:: c]).
proof: Proof. Proof using. by rewrite /walk_to_corner; case m => [| n] //= ->. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure