Theorem: BitTree.sub_toNat (Karatsuba.lean)

State before:
H : List Unit
x y : BitTree
inst✝¹ : Perfect H x
inst✝ : Perfect H y
⊢ ∀ {a b c d : ℕ}, a + b + c + d = a + (d + b + c)
Tactic:
intro _ _ _ _
State after:
H : List Unit
x y : BitTree
inst✝¹ : Perfect H x
inst✝ : Perfect H y
a✝ b✝ c✝ d✝ : ℕ
⊢ a✝ + b✝ + c✝ + d✝ = a✝ + (d✝ + b✝ + c✝)

State before:
H : List Unit
x y : BitTree
inst✝¹ : Perfect H x
inst✝ : Perfect H y
a✝ b✝ c✝ d✝ : ℕ
⊢ a✝ + b✝ + c✝ + d✝ = a✝ + (d✝ + b✝ + c✝)
Tactic:
ring
State after:
no goals