proposition: Lemma walk_to_corner_emptyr m rc (A B : seq nat) : (B == [::])%B -> mu (walk_to_corner m rc) (charfun A B) = 0.
proof: Proof. Proof using. move: rc => [r c] HB /=. apply: (mu_bool_negb0 _ (walk_to_corner_inv m r c)) => [] [X Y] /=. apply /implyP => /and4P[SX SY _ _]. move: SY; apply contra. by rewrite /charfun size_eq0 xpair_eqE (eqP HB); move => /andP[]. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure