proposition: Fact Z2Zp_opp u :〘-u〙= ∸〘u〙.
proof: Proof. apply Zp_plus_inj_l with (Z2Zp u). rewrite Zp_minus, <- Z2Zp_plus, <- Z2Zp_zero. f_equal; lia. 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)