simp [Nat.add_div inst.card_pos, Nat.div_eq_of_lt $ inst.encode_lt_card x]
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode ((encode xs * Fintype.card α + Encodable.encode x) / Fintype.card α) = x :: xs
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x ::
      decode
        (encode xs * Fintype.card α / Fintype.card α +
          if Fintype.card α ≤ Encodable.encode x % Fintype.card α then 1 else 0) =
    x :: xs