proposition: Fact Z2Zp_repr_canon u : { v |〘u〙=〘v〙 /\ 0 <= v < Z.of_nat p }.
proof: Proof. destruct (Z_pos_or_neg u); auto. apply Z2Zp_canon_neg; 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)