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