proposition: Lemma balanced_sumt0 w et : gram_balanced 0 false w -> matchg [::] et w -> sumt et = Color0.
proof: Proof. rewrite -(ccons_cbits (sumt et)) => balFw /matchg_balanced[-> bal0w]. by have [_ ->] := balanced_inj bal0w balFw. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)