norm_num
case succ.inl.«1»
n : ℕ
h : 2 ≤ 1 → ∏ x ∈ Ico 1 (succ 1), (↑x + 1) / ↑x = ↑1 + 1
hn : 2 ≤ 1 + 1
h✝ : 1 < 2
⊢ ((∏ x ∈ Ico 1 (1 + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (1 + 1), ↑x) * ((↑1 + 1 + 1) / (↑1 + 1)) = ↑1 + 1 + 1
no goals