proposition: Lemma match_count_0 st : (forall w, ~~ st w) -> forall bs et, match_count st bs et = 0.
proof: Proof. move=> st0 bs et; elim: et => [|e et IHet] in st bs st0 *. by rewrite /= (negPf (st0 _)). by case: e; rewrite /= ?IHet //; case: bs => * //=; rewrite IHet. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)