proposition: Lemma card_bal_hsz n : #|bal_hsz n| = 'C(n.*2, n).
proof: Proof. have := card_draws ('I_(n.*2) : finType) n; rewrite card_ord => <-. have /card_imset <- : injective (fun w => [set r : 'I_(n.*2) | preim (tnth w) (pred1 }}) r]). move => u v Huv; apply: eq_from_tnth => i. move: Huv => /(congr1 (fun s => i \in pred_of_set s)); rewrite !inE. by case: (tnth u i) (tnth v i) => [] []. congr #|pred_of_set _|; apply/setP => /= S. rewrite inE; apply/imsetP/idP => /= [[w Hw ->{S}] | /eqP HS]. - move: Hw; rewrite inE => /eqP Hw; apply/eqP. rewrite -[RHS](count_mem_height0 }} Hw). rewrite -(@card_preim_nth n.*2 _ _ _ {{) ?size_tuple //. by congr (#|pred_of_set _|); apply/setP => /= i; rewrite /= !inE -tnth_nth. - exists (mktuple (fun i => if i \in S then }} else {{)); first last. by apply/setP => /= i; rewrite inE tnth_mktuple /=; case: (i \in S). rewrite inE /height /=. do 2 rewrite -size_filter filter_map size_map. rewrite [X in (Posz (size X) - _)%R](eq_filter (a2 := mem (~: S))); first last. by move=> i; rewrite /= in_setC; case: (i \in S). rewrite [X in (_ - Posz (size X))%R](eq_filter (a2 := mem S)); first last. by move=> i /=; case: (i \in S). rewrite !enumT -/enum_mem -!cardE cardsCs. have -> : ~: ~: S = S by apply/setP => i; rewrite !inE negbK. by rewrite HS card_ord -addnn addnK subrr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree