proposition: Lemma right_sizes_from_left s : right_sizes (from_left s) = flatten [seq size_tree t :: right_sizes t | t <- rev s].
proof: Proof. elim: s => //= s0 s ->. by rewrite rev_cons -cats1 map_cat !flatten_cat /= cats0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype