proposition: Lemma Positive_tree_from_unfold : forall p, Positive_Tree_from p = LBin p (Positive_Tree_from (xO p)) (Positive_Tree_from (xI p)).
proof: Proof. intros p; now LTree_unfold (Positive_Tree_from p). Qed.
imports: Ltree building graft