exact Nat.div_le_self n inst.card
case h₁
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ sizeOf (n / Fintype.card α) ≤ ?m

case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ?m < sizeOf (Nat.succ n)

case m
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ℕ
case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ n < sizeOf (Nat.succ n)