proposition: Lemma enum_traceP (Alpha Beta : nat) : corner_box p (Alpha, Beta) -> forall A B, (A, B) \in enum_trace Alpha Beta = [&& (is_trace A B), (last 0 A == Alpha) & (last 0 B == Beta)].
proof: Proof. Proof using. move=> Hcorn A B. apply/idP/idP. - move=> /allpairsP[[eA eB] /= [HA HB [H1 H2]]]; subst eA eB. apply/and3P; split. + exact: (trace_corner_box Hcorn). + by move: HA => /mapP[A' _ ->]; rewrite last_rcons. + by move: HB => /mapP[B' _ ->]; rewrite last_rcons. - move=> /and3P[Htrace /eqP HlA /eqP HlB]. apply/allpairsP; exists (A, B) => /=; split; last by []. + by rewrite -HlA; exact: (trace_seqlP Htrace). + by rewrite -HlB; exact: (trace_seqrP Htrace). Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure