proposition: Lemma factor_Dyck_seq D : { DS : seq Dyck | D = foldr join_Dyck nil_Dyck DS }.
proof: Proof. elim/Dyck_ind: D => [|D1 D2 _ [DS IHD]]; first by exists [::]. by exists (D1 :: DS); rewrite IHD. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree