proposition: Fact Z2Zp_neg u : u <= 0 -> 〘u〙 = ∸〘-u〙.
proof: Proof. intros H. unfold Z2Zp at 1. destruct (Z_pos_or_neg u) as [ H' | H' ]; try lia; auto. replace u with 0 by lia. rewrite Z.opp_0, Z2Nat.inj_0, nat2Zp_zero, Z2Zp_zero; auto. symmetry; apply Zp_opp_zero. unfold Z2Zp. destruct (Z_pos_or_neg (-u)) as [ H'' | H'' ]; try lia; 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)