proposition: Fact Zp_minus : forall x, x ⊕ ∸ x = Zp.
proof: Proof. intros ([ | x ] & Hx); apply Zp_inj; simpl. + rewrite Nat.sub_0_r, rem_diag, rem_lt; auto. + rewrite rem_lt with (a := _ - _); try lia. replace (S (x+(p - S x))) with p by lia. apply rem_diag; 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)