proposition: Lemma size_count_braceE (w : seq brace) : size w = count_mem {{ w + count_mem }} w.
proof: Proof. elim: w => //= w0 w IHw. rewrite [(_ + count_mem }} w)%N]addnC !addnA. rewrite -[((w0 == {{) + count_mem _ _ + _)%N]addnA -IHw. by case: w0 => /=; rewrite ?addn0 ?add0n ?addn1 ?add1n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree