Theorem: incrSeqAux_eq_propagateCarry (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ (incrSeqAux x n).snd = propagateCarry (fun x => true) (fun carry bits x => bits () && carry ()) (fun x_1 => x) n ()
Tactic:
induction n <;> simp [incrSeqAux, *]
State after:
no goals