rw [h]
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = n.succ
⊢ i ∣ (n + 1) * fac n
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = n.succ
⊢ n.succ ∣ (n + 1) * fac n