diff options
Diffstat (limited to 'src/Util/ZUtil/AddGetCarry.v')
| -rw-r--r-- | src/Util/ZUtil/AddGetCarry.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v index e8f8d883d..5b8cbf13e 100644 --- a/src/Util/ZUtil/AddGetCarry.v +++ b/src/Util/ZUtil/AddGetCarry.v @@ -1,5 +1,4 @@ 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. @@ -64,7 +63,7 @@ Module Z. Z.add_get_carry_full Z.add_with_get_carry_full 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. + Z.sub_get_borrow Z.sub_with_get_borrow Z.sub_with_borrow Let_In. Lemma add_get_carry_full_mod s x y : fst (Z.add_get_carry_full s x y) = (x + y) mod s. |