proposition: Fact Zp_list_length : length Zp_list = p.
proof: Proof. unfold Zp_list; rewrite map_length, list_an_length; auto. 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)