proposition: Lemma prime2745982553 : prime 2745982553.
proof: Proof. apply (Pocklington_refl (Pock_certif 2745982553 3 ((191, 1)::(2,3)::nil) 167) ((Proof_certif 191 prime191) :: (Proof_certif 2 prime2) :: nil)). vm_cast_no_check (refl_equal true). Qed.
imports: PocklingtonRefl