proposition: Lemma trace_corner_box (Alpha Beta : nat) : corner_box p (Alpha, Beta) -> forall A B, A \in trace_seq Alpha -> B \in trace_seq Beta -> is_trace A B.
proof: Proof. Proof using. move=> Hcorn A B /mapP[[A' /= subA _ ->{A}]] /mapP[[B' /= subB _ ->{B}]]. by rewrite /is_trace !rcons_nilF /= -!sorted_subseq_iota_rcons subA subB !last_rcons. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure