proposition: Fact nat2Zp_surj u : { x | x < p /\ u = 〚x〛 }.
proof: Proof. destruct u as (u & Hu); exists u; split; auto. apply Zp_inj; simpl. rewrite rem_prop with (n := 0) (2 := Hu); 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)