proposition: Lemma is_trace_in_in_shape (A B : seq nat) : is_trace A B -> forall a b, a \in A -> b \in B -> in_shape p (a, b).
proof: Proof. Proof using. rewrite /is_trace => /and5P[_ _ HltnA HltnB /corner_box_in_part Hpart] a b Ha Hb. by apply: (@in_part_le p (last 0 A) (last 0 B) _ _ (intpartP p) Hpart); exact: sorted_in_leq_last. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure