diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-07-08 16:17:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-07-08 16:17:02 -0400 |
| commit | 59dec7e5b97b447e91a8d86440848f4c5d74c93f (patch) | |
| tree | f577b6f4b71c1f426823e9257af3c0db94b29a80 /src/Util/ZUtil/AddGetCarry.v | |
| parent | 86772a8a67e246ba93c708bdb0459f2f39edb966 (diff) | |
More fine-grained tactics imports
Diffstat (limited to 'src/Util/ZUtil/AddGetCarry.v')
| -rw-r--r-- | src/Util/ZUtil/AddGetCarry.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v index 18822cbe3..e8897431a 100644 --- a/src/Util/ZUtil/AddGetCarry.v +++ b/src/Util/ZUtil/AddGetCarry.v @@ -2,10 +2,11 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Hints.ZArith. -Require Import Crypto.Util.Prod Crypto.Util.Tactics. +Require Import Crypto.Util.Prod. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. Local Notation eta x := (fst x, snd x). @@ -62,7 +63,7 @@ Module Z. Z.add_get_carry Z.add_with_get_carry Z.add_with_carry Z.sub_get_borrow_full Z.sub_with_get_borrow_full Z.sub_get_borrow Z.sub_with_get_borrow Z.sub_with_borrow. - + Lemma add_get_carry_full_mod s x y : fst (Z.add_get_carry_full s x y) = (x + y) mod s. Proof. easypeasy. Qed. |