proposition: Fact Z2Zp_pos u : 0 <= u -> 〘u〙= 〚Z.to_nat u〛.
proof: Proof. intros H. unfold Z2Zp. destruct (Z_pos_or_neg u); try lia; 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)