proposition: Fact nat2Zp_minus_one : 〚p-1〛= ∸Op.
proof: Proof. rewrite nat2Zp_minus; try lia. rewrite nat2Zp_p, nat2Zp_one; ring. 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)