proposition: Lemma size_cat_left t u : size_tree (cat_left t u) = size_tree t + size_tree u.
proof: Proof. rewrite /cat_left size_from_left map_cat sumn_cat. by rewrite -!size_from_left !left_branchK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype