proposition: Lemma trace_seqrP (A B : seq nat) : is_trace A B -> B \in trace_seq (last 0 B).
proof: Proof. Proof using. move=> /and5P[]. case/lastP: B => // B lB _ _ _ Hsort /= _. rewrite last_rcons /trace_seq; apply/mapP => /=. have subB : subseq B (iota 0 lB) by rewrite sorted_subseq_iota_rcons. by exists (Subseqs subB); first exact: mem_enum. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure