proposition: Lemma size_tracer (a b : nat) (A B : seq nat) : is_trace (a :: A) (b :: B) -> size B < hook_length p (a, b).
proof: Proof. Proof using. move=> /trace_size_arm_length/leq_trans; apply. by rewrite leq_addr. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure