proposition: Fact Z2Zp_of_nat n : 〘Z.of_nat n〙 = 〚n〛.
proof: Proof. rewrite Z2Zp_pos, Nat2Z.id; auto. apply Zle_0_nat. 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)