simp [Nat.fin_mod, Nat.mul_comm, Nat.div_add_mod n inst.card]
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ n / Fintype.card α * Fintype.card α + ↑(Nat.fin_mod n ⋯) = n
no goals