Factorial

\import Algebra.Ordered
\import Arith.Nat
\import Function.Meta
\import Order.StrictOrder
\import Paths.Meta

\func fac (n : Nat) : Nat
  | 0 => 1
  | suc n => suc n Nat.* fac n

\lemma fac>0 {n : Nat} : 0 < fac n \elim n
  | 0 => NatSemiring.zero<suc
  | suc n => rewrite NatSemiring.*-comm $ LinearlyOrderedAbMonoid.<=_+-left zero<=_ fac>0