induction' n with n ih
i n : ℕ
ipos : 0 < i
ile : i ≤ n
⊢ i ∣ fac n
case zero
i : ℕ
ipos : 0 < i
ile : i ≤ 0
⊢ i ∣ fac 0

case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ fac (n + 1)