have hk' : k / f 0 < Fin.prod (f ∘ succ) := by
  rw [Nat.div_lt_iff_lt_mul hpos]
  rw [Nat.mul_comm, ←prod_succ]
  exact hk
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0
case a.left.e_a.e_a
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
k : Nat
hk : k < prod f
h : decodePi f ⟨k, hk⟩ = x
hpos : f 0 > 0
hk' : k / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) = k / f 0