Primality prover #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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