Theorem: decrSeqAux_eq_propagateCarry (Lean4bits/lemmas.lean)

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