proposition: Fact nat2Zp_inj u v : 〚u〛=〚v〛 <-> rem u p = rem v p.
proof: Proof. split; intros H. + apply f_equal with (f := @proj1_sig _ _) in H; auto. + apply Zp_inj; 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)