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