simp [decode, FinDenumerable.decode_fin]
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (decode (Nat.succ n)) = Nat.succ n
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (Option.get (Encodable.decode ↑(Nat.fin_mod n ⋯)) ⋯ :: decode (n / Fintype.card α)) = Nat.succ n