proposition: Fact Zp_plus_inj_l x y z : x ⊕ y = x ⊕ z -> y = z.
proof: Proof. intros H. apply f_equal with (f := fun a => ∸ x ⊕ a) in H. do 2 rewrite Zp_add_assoc in H. rewrite (Zp_add_comm _ x), Zp_minus in H. do 2 rewrite Zp_plus_zero in H; 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)