proposition: Lemma match_countP (st : spec_gtree) bs et : reflect (exists2 w, st w & matchpg bs et w) (match_count st bs et != 0).
proof: Proof. elim: et => /= [|e et IHet] in st bs *. case: ifP => st0; constructor; first by exists [::]. by case=> [] [|[]] //; rewrite st0. case: e; try (rewrite addn_eq0 negb_and; case: (IHet) => [pushMet | ]; first by [left; have [w] := pushMet; exists (Gpush :: w)]; case: bs => [|bs|bs] not_pushMet); do [right | apply: (iffP (IHet _ _)) => [[w]|]]; by [exists (Gpop0 :: w) | exists (Gpop1 :: w) | exists (Gskip :: w) | case=> [] [|[] w] // *; by [exists w | case: not_pushMet; exists w]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)