fact: Fixpoint test_Certif (lc : Certif) : bool := match lc with | nil => true | (Proof_certif _ _) :: lc => test_Certif lc | (Lucas_certif n p) :: lc => let xx := test_Certif lc in if xx then let yy := gt2 p in if yy then match p with Zpos p1 => let zz := Mp p in match zz with | Zpos n' => if (n ?= n')%P then let tt := lucas p1 in match tt with | Z0 => true | _ => false end else false | _ => false end | _ => false end else false else false | (Pock_certif n a dec sqrt) :: lc => let xx := test_pock n a dec sqrt in if xx then let yy := all_in lc dec in (if yy then test_Certif lc else false) else false | (SPock_certif n a dec) :: lc => let xx :=test_spock n a dec in if xx then let yy := all_in lc dec in (if yy then test_Certif lc else false) else false | (Ell_certif n ss l a b x y) :: lc => let xx := ell_test n ss l a b x y in if xx then let yy := all_in lc l in if yy then test_Certif lc else false else false end.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) Pmod Mod_op W Lucas PocklingtonCertificat NEll Bits