proposition: Lemma rem_eq_eq a b v : 2*a < v -> 2*b < v -> rem a v = rem b v -> a = b.
proof: Proof. intros H1 H2 H3. do 2 (rewrite rem_lt in H3; try lia). Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)