[GOAL]
α : Type u
x : Tree α
⊢ numLeaves x = numNodes x + 1
[PROOFSTEP]
induction x
[GOAL]
case nil
α : Type u
⊢ numLeaves nil = numNodes nil + 1
[PROOFSTEP]
simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
[GOAL]
case node
α : Type u
a✝² : α
a✝¹ a✝ : Tree α
a_ih✝¹ : numLeaves a✝¹ = numNodes a✝¹ + 1
a_ih✝ : numLeaves a✝ = numNodes a✝ + 1
⊢ numLeaves (node a✝² a✝¹ a✝) = numNodes (node a✝² a✝¹ a✝) + 1
[PROOFSTEP]
simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
[GOAL]
α : Type u
x : Tree α
⊢ 0 < numLeaves x
[PROOFSTEP]
rw [numLeaves_eq_numNodes_succ]
[GOAL]
α : Type u
x : Tree α
⊢ 0 < numNodes x + 1
[PROOFSTEP]
exact x.numNodes.zero_lt_succ
[GOAL]
α : Type u
h : nil ≠ nil
⊢ node () (left nil) (right nil) = nil
[PROOFSTEP]
trivial
