fact: Definition test_pock N a dec sqrt := if (2 ?< N) then let Nm1 := Pos.pred N in let F1 := mkProd dec in match (Nm1 / F1)%P with | (Npos R1, N0) => if is_odd R1 then if is_even F1 then if (1 ?< a) then let (s,r') := (R1 / (xO F1))%P in match r' with | Npos r => if (a ?< N) then let op := cmk_op (Peano.pred (nat_of_P (get_height 63 (plength N)))) in let wN := znz_of_Z op (Zpos N) in let wa := znz_of_Z op (Zpos a) in let w1 := znz_of_Z op 1 in let mod_op := make_mod_op op wN in let pow := mod_op.(power_mod) in let ttimes := mod_op.(mul_mod) in let pred:= mod_op.(pred_mod) in let gcd:= ZnZ.gcd in let A := pow_mod_pred _ mod_op (pow wa R1) dec in match all_pow_mod _ mod_op w1 A dec with | (p, aNm1) => match ZnZ.to_Z aNm1 with (Zpos xH) => match ZnZ.to_Z (gcd p wN) with (Zpos xH) => if check_s_r s r sqrt then (N ?< (times ((times ((xO F1)+r+1) F1) + r) F1) + 1) else false | _ => false end | _ => false end end else false | _ => false end else false else false else false | _=> false end else false.
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