proposition: Fact Zp_add_assoc : forall x y z, x ⊕ (y ⊕ z) = x ⊕ y ⊕ z.
proof: Proof. intros (x & ?) (y & ?) (z & ?); apply Zp_inj; simpl. rewrite (Nat.add_comm (rem _ _) z), rem_plus_rem, rem_plus_rem. f_equal; ring. 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)