have ih := @decodenk α _ (n / inst.card)
α : Type u_1
inst : Alphabet α
n : ℕ
⊢ encode (decode (Nat.succ n)) = Nat.succ n
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (decode (Nat.succ n)) = Nat.succ n