proposition: Lemma size_right_sizes t : size (right_sizes t) = size_tree t.
proof: Proof. elim: t => //= l <- r <-. by rewrite size_cat /= addnS add1n addSn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype