induction' n with n ih
case succ
n : ℕ
⊢ 2 ^ (n + 1 - 1) ≤ fac (n + 1)
case succ.zero

⊢ 2 ^ (0 + 1 - 1) ≤ fac (0 + 1)

case succ.succ
n : ℕ
ih : 2 ^ (n + 1 - 1) ≤ fac (n + 1)
⊢ 2 ^ (n + 1 + 1 - 1) ≤ fac (n + 1 + 1)