fix Montgomery proof and clean up a little

1 files changed, 11 insertions, 0 deletions

diff --git a/src/Fancy/Prod.v b/src/Fancy/Prod.v
index a3f72f17d..a46a7a4f0 100644
--- a/src/Fancy/Prod.v
+++ b/src/Fancy/Prod.v
@@ -375,4 +375,15 @@ Ltac push_value_unused :=
          | _ => apply not_in_cons; split;
                 [ try assumption; symmetry; assumption | ]
          | _ => apply in_nil
+         end.
+
+(* Solves subgoals for commutativity proofs and simplifies register
+lookup expressions *)
+Ltac simplify_with_register_properties :=
+  repeat match goal with
+         | _ => rewrite reg_eqb_refl
+         | _ => rewrite reg_eqb_neq by congruence
+         | H : ?y = _ mod ?m |- 0 <= ?y < _ =>
+           rewrite H; apply Z.mod_pos_bound; lia
+         | _ => assumption
          end.
\ No newline at end of file