rw [<- inst.encode_fin_eq_encode _, inst.decodenk]
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ n / Fintype.card α * Fintype.card α + Encodable.encode (FinDenumerable.decode_fin (Nat.fin_mod n ⋯)) = n
α : 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