proposition: Lemma trace_size_leg_length (a b : nat) (A B : seq nat) : is_trace (a :: A) (b :: B) -> size A <= leg_length p (a, b).
proof: Proof. Proof using. elim: A a => // A0 A IHA a /= Htrace. apply: (leq_ltn_trans (IHA _ (is_trace_tll _ Htrace))); first by []. have:= Htrace => /and5P[_ _ /= /andP[Ha _] _ _]. rewrite {IHA} /leg_length. suff HA0 : A0 < nth 0 conj b. rewrite -ltnS prednK; last by rewrite subn_gt0. rewrite -ltnS prednK //; last by rewrite subn_gt0; exact: (ltn_trans Ha HA0). rewrite ltnS; apply ltn_sub2l; last exact Ha. exact: (ltn_trans Ha HA0). rewrite -/(in_shape _ (_, _)). rewrite -in_conj_part //. by apply (is_trace_in_in_shape Htrace); rewrite !inE eq_refl /= ?orbT. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure