proposition: Lemma trace_size_arm_length (a b : nat) (A B : seq nat) : is_trace (a :: A) (b :: B) -> size B <= arm_length p (a, b).
proof: Proof. Proof using. elim: B b => // B0 B IHB b /= Htrace. apply: (leq_ltn_trans (IHB _ (is_trace_tlr _ Htrace))); first by []. have:= Htrace => /and5P[_ _ _ /= /andP[Hb _] _]. rewrite {IHB} /arm_length. suff HB0 : B0 < nth 0 p a. rewrite -ltnS prednK; last by rewrite subn_gt0. rewrite -ltnS prednK //; last by rewrite subn_gt0; exact: (ltn_trans Hb HB0). rewrite ltnS; apply ltn_sub2l; last exact Hb. exact: (ltn_trans Hb HB0). rewrite -/(in_shape _ (_, _)). 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