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