proposition: Lemma height_cat u v : height (u ++ v) = height u + height v.
proof: Proof. rewrite /height !count_cat !PoszD [X in -X]addrC opprD -!addrA; congr (_ + _). by rewrite [RHS]addrC addrA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree