fact: Definition choose_corner : distr ((seq nat) * (seq nat)) := Mlet (Random (sumn p).-1) (fun n => let (r, c) := (reshape_index p n, reshape_offset p n) in walk_to_corner (hook_length p (r, c)).-1 (r, c)).
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure