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