proposition: Lemma foldr_join_Dyck_inj : injective (foldr join_Dyck nil_Dyck).
proof: Proof. by elim => [|D1 DS1 IHDS1] [|D2 DS2] // /join_Dyck_inj [-> /IHDS1 ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree