proposition: Fact divides_nat2Zp u : divides p u <-> 〚u〛= Zp.
proof: Proof. split. + intros (q & Hq); apply Zp_inj; simpl. apply rem_prop with q; lia. + intros H. apply f_equal with (f := @proj1_sig _ _) in H; simpl in H. exists (div u p). rewrite (div_rem_spec1 u p) at 1; 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)