proposition: Theorem Dyck_ind D : P D.
proof: Proof. move: {2}(size D) (leqnn (size D)) => n. elim: n D => [|n IHn] D. rewrite leqn0 => /nilP H. by have -> : D = nil_Dyck by apply: val_inj. case: (D =P nil_Dyck) => [-> // | /eqP/factor_Dyck [[D1 D2] /= ->]]. rewrite /= ltnS size_cat /= addnS => /ltnW Hsz. apply: Pcons; apply IHn. - exact: (leq_trans (leq_addr (size D2) (size D1))). - exact: (leq_trans (leq_addl (size D1) (size D2))). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree