Library PrimeGapS1.Witness_Rayleigh
From Stdlib Require Import ZArith List.
Import ListNotations.
Open Scope Z_scope.
Definition v_witness : list (Z × Z) :=
[
((-1)%Z, 67213321643309%Z) ;
((-1)%Z, 127608469198%Z) ;
(1%Z, 279653882552%Z) ;
((-1)%Z, 12020445731%Z) ;
(1%Z, 549859441%Z) ;
((-1)%Z, 1793413588%Z) ;
((-1)%Z, 2852111653%Z) ;
(1%Z, 39510722%Z) ;
(3%Z, 12111503%Z) ;
((-1)%Z, 5889766%Z) ;
((-1)%Z, 3065036%Z) ;
((-11)%Z, 16762960%Z) ;
(1%Z, 56351289%Z) ;
((-4)%Z, 1502055%Z) ;
((-368)%Z, 7848717%Z) ;
((-248)%Z, 7629181%Z) ;
(83%Z, 10305760%Z) ;
(874%Z, 12663047%Z) ;
(2999%Z, 13498748%Z) ;
(389%Z, 4466540%Z) ;
((-3)%Z, 6400234%Z) ;
(1277%Z, 10688233%Z) ;
(11484%Z, 3794749%Z) ;
(39537%Z, 8813404%Z) ;
(6952%Z, 10377483%Z) ;
((-6142)%Z, 31211377%Z) ;
((-227846)%Z, 52361791%Z) ;
((-150115)%Z, 7175034%Z) ;
((-250783)%Z, 22648711%Z) ;
(37237%Z, 12498809%Z) ;
(67%Z, 12886771%Z) ;
((-35583)%Z, 17941657%Z) ;
((-522509)%Z, 7595235%Z) ;
((-1507327)%Z, 7740852%Z) ;
((-365121)%Z, 2548910%Z) ;
((-499886)%Z, 13468967%Z) ;
(14389%Z, 7143324%Z) ;
(5289169%Z, 57282634%Z) ;
(11505763%Z, 16419588%Z) ;
(1%Z, 1%Z) ;
(15488075%Z, 35377856%Z) ;
(312214%Z, 4565683%Z)
].