proposition: Lemma walk_to_corner0_simpl r c : walk_to_corner 0 (r, c) = Munit ([:: r], [:: c]).
proof: Proof. Proof using. by []. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure