proposition: Fact Zp_plus_zero : forall x, Zp ⊕ x = x.
proof: Proof. intros (x & Hx); apply Zp_inj; simpl. apply rem_prop with 0; simpl; 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)