fact: Definition trace_seq (last : nat) : seq (seq nat) := [seq rcons tr last | tr : subseqs (iota 0 last)].
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure