proposition: Lemma is_trace_lastr (a b : nat) (A B : seq nat) : is_trace (a :: A) (b :: B) -> is_trace (a :: A) [:: last b B].
proof: Proof. Proof using. elim: B b => // B0 B IHB b /= /is_trace_tlr H. have {}/H : B0 :: B != [::] by []. exact: IHB. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure