proposition: Fact Z2Zp_morphishm : ring_morphism 0%Z 1%Z Zplus Zmult Z.opp (Zp_zero Hp) (Zp_one Hp) (Zp_plus Hp) (Zp_mult Hp) (Zp_opp Hp) (Z2Zp Hp).
proof: Proof. exists. + apply Z2Zp_zero. + apply Z2Zp_one. + apply Z2Zp_plus. + apply Z2Zp_mult. + apply Z2Zp_opp. 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)