simp [addWithCarry, @addWithCarry_eq_ofNat_add H, rearrange, toNat_node, bound_cons,
  ← Nat.div_div_eq_div_mul, Nat.mul_add_div (bound_pos _),  divBound]
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
rearrange : ∀ {m xh xl yh yl c : ℕ}, m * xh + xl + (m * yh + yl) + c = m * (xh + yh) + (xl + yl + c)
⊢ addWithCarry (node l✝¹ r✝¹) (node l✝ r✝) x✝ =
    ({ val := (toNat (() :: H) (node l✝¹ r✝¹) + toNat (() :: H) (node l✝ r✝) + ↑x✝) / bound (() :: H),
        isLt := (_ : (toNat (() :: H) (node l✝¹ r✝¹) + toNat (() :: H) (node l✝ r✝) + ↑x✝) / bound (() :: H) < 2) },
      ofNat (() :: H) (toNat (() :: H) (node l✝¹ r✝¹) + toNat (() :: H) (node l✝ r✝) + ↑x✝))
no goals