fact: Fixpoint all_in (lc : Certif) (lp : dec_prime) {struct lp} : bool := match lp with | nil => true | (p,_) :: lp => if all_in lc lp then is_in p lc else false end.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod