proposition: Lemma size_from_left s : size_tree (from_left s) = sumn [seq (size_tree t).+1 | t <- s].
proof: Proof. by elim: s => //= s0 s <-; rewrite add1n !addSn addnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype