fact: Definition hook_box rc n : nat * nat := match n with inl k => (k,rc.2) | inr k => (rc.1,k) end.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure