proposition: Lemma is_trace_tll a A B : A != [::] -> is_trace (a :: A) B -> is_trace A B.
proof: Proof. Proof using. rewrite /is_trace => HA /and5P[_ -> /path_sorted -> ->]. by rewrite HA /=; case: A HA. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure