proposition: Lemma walk_to_corner_simpl m r c : forall (Hs : (size (hook_box_indices (r, c)) != 0)), walk_to_corner m.+1 (r, c) = Mlet (Uniform (mkunif (hook_box_indices (r, c)) Hs)) (fun n => match n with | inl k => Mlet (walk_to_corner m (k, c)) (fun X => Munit (r::X.1, X.2)) | inr k => Mlet (walk_to_corner m (r, k)) (fun X => Munit (X.1, c::X.2)) end).
proof: Proof. Proof using. by rewrite /walk_to_corner /=; case: hook_box_indices. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure