proposition: Lemma match_count_balanced h et : match_count (init_gtree_spec h) Bstack0 et = if (size et == h) && (Color0 \notin ctrace et) then dyck (count_cbit1 (ctrace et)) else 0.
proof: Proof. rewrite /init_gtree_spec /ctrace /dyck; pose sb : bitseq := [::]. rewrite -[Bstack0]/(stack_of_bitseq sb) -{-4}[0]/(size sb) -(add0c (sumt et)). have c1_lb: cbit1 Color0 = odd (size sb) by []. pose sbs := foldr addb false. have c0_lb: cbit0 Color0 = false (+) sbs sb by []. elim: et h {-3}Color0 sb false c0_lb c1_lb => [|e et IHet] h c lb b0. case: h lb => [|h] [|b lb] //=; first by rewrite addbF => <-; case: c. by case: c b0 (size lb) => [] [] []. rewrite /= addcA; case: h => [|h c0lb c1lb]. by case: e (stack_of_bitseq lb) => [] [|sb|sb] //=; rewrite ?match_count_0. have{IHet} := IHet h (e +c c). rewrite cbit0_addc cbit1_addc (addcC e c) {}c0lb {}c1lb /= inE eqSS. move: (size et == h) {c}(Color0 \in _) (count_cbit1 _) => b_h bc0 i IHet. have /= IHet0 := IHet (cbit0 e :: lb) b0. rewrite /= 2!addbA (addbC b0) in IHet IHet0 *. case: e in IHet IHet0 *; rewrite ?andbF //=; first exact: IHet; by rewrite {}IHet0 //; case: lb IHet => [_ | b lb'']; [ case: {3}i => *; rewrite /= ?addn0 | rewrite ?negbK 1?addbA -1?(addbC b); case: b => /= ->; rewrite ?negbK //; case: (b_h && ~~ bc0)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree dyck)