proposition: Fact nat2Zp_divides u v :〚u〛=〚v〛-> divides p u -> divides p v.
proof: Proof. intros H. apply f_equal with (f := @proj1_sig _ _) in H; simpl in H. do 2 (rewrite divides_rem_eq; auto); 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)