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