def factorial_pos

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/fact.bend:43

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend as S

43# 0 < n!   (Mathlib Nat.factorial_pos)
44def factorial_pos(+n: Nat) -> {Nat.is_lt(0n, S.factorial(n)) == True{} : Bool}:
45  match n:
46    case 0n:
47      {==}
48    case 1n+ +p:
49      pos_mul(p, S.factorial(p), factorial_pos(p))