diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-20 18:53:24 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-07-20 18:53:43 -0400 |
| commit | 980c92a3b46897b4e1b1d72bc552d3a48e27c673 (patch) | |
| tree | 48245e423b8a37a36fe8f8fdf79cda77be1a86ea /src/ModularArithmetic | |
| parent | d7f30db5fe04b11fa22a3b3b79eb0e63a72cb0f1 (diff) | |
automate a proof
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/Pre.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 47a38b867..5e61278f6 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -4,6 +4,7 @@ Require Import Coq.Logic.EqdepFacts. Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.omega.Omega. Require Import Crypto.Util.NumTheoryUtil. +Require Import Crypto.Tactics.VerdiTactics. Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. symmetry. @@ -106,7 +107,7 @@ Program Definition mod_inv_sig {m} (a:{z : Z | z = z mod m}) : {z : Z | z = z mo | _ => powmod m a (Z.to_N (m-2)) end. Next Obligation. - abstract (destruct a; rewrite ?powmod_Zpow_mod, ?Zmod_mod, ?Zmod_0_l; reflexivity). + intros; break_match; rewrite ?powmod_Zpow_mod, ?Zmod_mod, ?Zmod_0_l; reflexivity. Qed. Program Definition inv_impl {m : BinNums.Z} : |