diff options
Diffstat (limited to 'src/Util/ZUtil/AddGetCarry.v')
| -rw-r--r-- | src/Util/ZUtil/AddGetCarry.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v index 0208207b3..34f5f2ea8 100644 --- a/src/Util/ZUtil/AddGetCarry.v +++ b/src/Util/ZUtil/AddGetCarry.v @@ -70,4 +70,8 @@ Module Z. reflexivity. Qed. + Lemma sub_with_borrow_to_add_get_carry c x y + : Z.sub_with_borrow c x y = Z.add_with_carry (-c) x (-y). + Proof. reflexivity. Qed. + End Z. |