fact: Definition check_s_r s r sqrt := match s with | N0 => true | Npos p => match (Zminus (square r) (xO (xO (xO p)))) with | Zpos x => let sqrt2 := square sqrt in let sqrt12 := square (Pos.succ sqrt) in if sqrt2 ?< x then x ?< sqrt12 else false | Zneg _ => true | Z0 => false end end.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod