proposition: Fact Zp_list_spec x : In x Zp_list.
proof: Proof. destruct (nat2Zp_surj x) as (n & H1 & H2); subst. apply in_map_iff; exists n; split; auto. apply list_an_spec; lia. Qed.
imports: Arith Lia ZArith List Permutation Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime binomial sums php) Undecidability.H10.ArithLibs(matrix)