proposition: Fact Z2Zp_zero : 〘0〙= Zp.
proof: Proof. rewrite Z2Zp_pos; try lia. rewrite Z2Nat.inj_0, nat2Zp_zero; 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)