Theorem: negSeqAux_eq_propagateCarry (Lean4bits/lemmas.lean)

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