proposition: Lemma size_left_branch t : all (fun l => size_tree l < size_tree t) (left_branch t).
proof: Proof. rewrite -{1}(left_branchK t) size_from_left. elim: (left_branch t) => //= l lb /allP IHlb. rewrite {1}addSn ltnS leq_addr /=. apply/allP => t1 /IHlb /leq_trans; apply. exact: leq_addl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype