proposition: Lemma prime621072748687 : prime 621072748687.
proof: Proof. apply (Pocklington_refl (Pock_certif 621072748687 3 ((7962471137, 1)::(2,1)::nil) 1) ((Pock_certif 7962471137 3 ((248827223, 1)::(2,5)::nil) 1) :: (Pock_certif 248827223 5 ((601, 1)::(2,1)::nil) 265) :: (Proof_certif 601 prime601) :: (Proof_certif 2 prime2) :: nil)). vm_cast_no_check (refl_equal true). Qed.
imports: PocklingtonRefl