proposition: Lemma match_count_partition st st' st'' : sgtree_partition st st' st'' -> forall bs et, match_count st bs et = match_count st' bs et + match_count st'' bs et.
proof: Proof. move=> eq_st bs et; elim: et => [|e et IHet] in st st' st'' eq_st bs *. by have /= := eq_st [::]; case: (st _); case: (st' _); case: (st'' _). case: e => //=; try (rewrite addnCA -addnA addnCA addnA; case: bs => *; congr (_ + _)); by apply: IHet => w; apply: eq_st. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)