Primality prover #
This file provides a
norm_num extention to prove that natural numbers are prime.
A predicate representing partial progress in a proof of
A partial proof of
factors. Asserts that
l is a sorted list of primes, lower bounded by a
p, which multiplies to