proposition: Lemma even_dyck_pos n : 0 < dyck n.*2.
proof: Proof. rewrite -[n.*2]addn0 /dyck; elim: n {-1}0 => [|n IHn] m. by rewrite gen_dyck_all_close. by rewrite doubleS addSnnS addSn ltn_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)