proposition: Lemma bintree_of_join_Dyck D1 D2 : bintree_of_Dyck ([Dyck {{ D1 }} D2]) = BinNode (bintree_of_Dyck D1) (bintree_of_Dyck D2).
proof: Proof. rewrite {1}/bintree_of_Dyck. case: (bintree_of_Dyck_spec _) => /= [[|t1 t2 /=] []]; first by move/eqP. move/join_Dyck_inj => [H1 H2]; apply. by rewrite /= !bintree_of_DyckK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree