proposition: Fact Zp_repr_interval a b u : Z.of_nat p <= b-a -> { v |〘u〙=〘v〙/\ a <= v < b }.
proof: Proof. intros Hab. destruct (Z2Zp_repr_canon (u-a)) as (v & H1 & H2). exists (a+v)%Z; split; try lia. rewrite Z2Zp_plus, <- H1, Z2Zp_minus; ring. 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)