def fac : ℕ → ℕ

Equations

• fac 0 = 1
• fac n.succ = (n + 1) * fac n

theorem fac_pos (n : ℕ) : 0 < fac n