proposition: Theorem Dyck_of_bintreeK t : bintree_of_Dyck (Dyck_of_bintree t) = t.
proof: Proof. elim: t => [|l IHl r IHr] /=; first exact: bintree_of_nil_Dyck. by rewrite bintree_of_join_Dyck IHl IHr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree