induction' n with n h
n : ℕ
hn : 2 ≤ n
⊢ ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
case zero
hn : 2 ≤ 0
⊢ ∏ x ∈ Ico 1 (succ 0), (↑x + 1) / ↑x = ↑0 + 1

case succ
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
⊢ ∏ x ∈ Ico 1 (n + 1).succ, (↑x + 1) / ↑x = ↑(n + 1) + 1