proposition: Fact Z2Zp_minus u v : 〘u-v〙 = 〘u〙⊕ ∸〘v〙.
proof: Proof. replace (u-v) with (u+(-v)) by lia. rewrite Z2Zp_plus; f_equal. 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)