simp [Nat.not_le_of_lt _, Nat.mod_lt _ inst.card_pos, ih]
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode (encode xs + if ¬Fintype.card α ≤ Encodable.encode x % Fintype.card α then 0 else 1) = x :: xs
no goals