Theorem: addSeqAux_eq_propagateCarry (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ (addSeqAux x y n).snd =
    propagateCarry (fun x => false)
      (fun carry bits x => bits true && bits false || bits false && carry () || bits true && carry ())
      (fun b => bif b then x else y) n ()
Tactic:
induction n <;> simp [addSeqAux, *]
State after:
no goals