Theorem: subSeqAux_eq_propagateCarry (Lean4bits/lemmas.lean)

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