proposition: Lemma Dyck_size_even s: Dyck_path s -> size s = (size s)./2.*2.
proof: Proof. by move /Dyck_path_size => ->; rewrite half_double. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)