proposition: Lemma well_founded_subtree' : well_founded subtree.
proof: Proof. apply wf_incl with (fun t t' => size t < size t'). intros x y Hxy; now apply subtree_smaller. apply wf_inverse_image; apply lt_wf. Qed.
imports: Lia Inverse_Image Wellfounded.Inclusion Wf_nat