rw [Nat.add_mul_div_left _ _ hpos]
case refl.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)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) =
    (↑(x 0) + f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)) / f 0
case refl.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)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
hpos : f 0 > 0
hk : f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0) < prod f
hk' : (f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0)) / f 0 < prod (f ∘ succ)
⊢ ↑(encodePi (fun i => f i.succ) fun i => x i.succ) = ↑(x 0) / f 0 + ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩)