fact: Fixpoint is_in (p : positive) (lc : Certif) {struct lc} : bool := match lc with | nil => false | c :: l => if p ?= (nprim c) then true else is_in p l end.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod