proposition: Lemma Dyck_size_even (D : Dyck) : ~~ odd (size D).
proof: Proof. elim/Dyck_ind: D => //= D1 D2 /negbTE HD1 /negbTE HD2. by rewrite size_cat /= addnS /= negbK oddD negb_add HD1 HD2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree