proposition: Lemma Pocklington_refl : forall c lc, test_Certif (c::lc) = true -> prime (nprim c).
proof: Proof. intros c lc Heq;apply test_Certif_In_Prime with (c::lc);trivial;simpl;auto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod