proposition: Lemma walk_to_corner_inv m r c : mu (walk_to_corner m (r, c)) (fun HS => [&& size HS.1 != 0, size HS.2 != 0, head 0 HS.1 == r& head 0 HS.2 == c]%N%:Q) = 1.
proof: Proof. Proof using. elim: m r c => [| n Hn] r c. by rewrite /= 2!eq_refl. case (size (hook_box_indices (r, c)) =P 0%N) => [H0 | /eqP Hs]. - by rewrite walk_to_corner_end_simpl //= !eq_refl. - rewrite (walk_to_corner_simpl _ Hs). rewrite Mlet_simpl mu_one_eq //. move => [] k /=. + apply: (mu_bool_impl1 _ (Hn k c)) => [] [A B] /=. apply /implyP => /and4P[_ H2 _ H4]. by rewrite H2 H4 eq_refl. + apply: (mu_bool_impl1 _ (Hn r k)) => [] [A B] /=. apply /implyP => /and4P[H1 _ H3 _]. by rewrite H1 H3 eq_refl. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure