proposition: Lemma count_mem_height0 n (w : n.*2.-tuple brace) b : height w = 0 -> count_mem b w = n.
proof: Proof. move=> /eqP; rewrite /height subr_eq0 eqz_nat => /eqP Heq. have:= size_count_braceE w. rewrite size_tuple Heq addnn => /double_inj {-1}->. by case b. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree