proposition: Lemma matchg_balanced et w : matchg [::] et w -> cbit1 (sumt et) = false /\ gram_balanced 0 (cbit0 (sumt et)) w.
proof: Proof. set sb := [::]; rewrite -[cbit1 _]addFb -[cbit0 _]addFb -{3}[false]/(sumb sb). rewrite -{1}[false]/(odd 0) -[0]/(size sb). elim: et sb w => [|e et IHet] lb [|s w] //=; first by case: lb. rewrite cbit0_addc cbit1_addc 2!addbA -addTb. rewrite -(addbC (cbit0 e)) -(addbC (cbit1 e)) !addbA. case: s {IHet}(IHet (cbit0 e :: lb) w) (IHet lb w) (IHet (behead lb) w); by case: e => //; case: lb => [|[|] lb] //=; rewrite ?negbK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)