Add Zmod_to_equiv_modulo

1 files changed, 9 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 42e88e8c4..a82cd7cda 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -3018,3 +3018,12 @@ Ltac Ztestbit_step :=
   | _ => progress Ztestbit_full_step
   end.
 Ltac Ztestbit := repeat Ztestbit_step.
+
+(** Change [_ mod _ = _ mod _] to [Z.equiv_modulo _ _ _] *)
+Ltac Zmod_to_equiv_modulo :=
+  repeat match goal with
+         | [ H : context T[?x mod ?M = ?y mod ?M] |- _ ]
+           => let T' := context T[Z.equiv_modulo M x y] in change T' in H
+         | [ |- context T[?x mod ?M = ?y mod ?M] ]
+           => let T' := context T[Z.equiv_modulo M x y] in change T'
+         end.