Theorem: BitTree.addWithCarry_negate (Karatsuba.lean)

State before:
H : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
⊢ addWithCarry (node l✝ r✝) (negate (node l✝ r✝)) 1 = (1, ofNat (() :: H) 0)
Tactic:
simp [addWithCarry, addWithCarry_negate (H := H)]
State after:
no goals