add wrapper for add_get_carry and proofs for add_get_carry and zselect

1 files changed, 16 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Zselect.v b/src/Util/ZUtil/Zselect.v
new file mode 100644
index 000000000..0166ce6f4
--- /dev/null
+++ b/src/Util/ZUtil/Zselect.v
@@ -0,0 +1,16 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.Tactics.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma zselect_correct cond zero_case nonzero_case :
+    Z.zselect cond zero_case nonzero_case =
+    if dec (cond = 0) then zero_case else nonzero_case.
+  Proof.
+    cbv [Z.zselect]; break_match;
+      try reflexivity; try discriminate.
+    rewrite <-Z.eqb_neq in *; congruence.
+  Qed.
+End Z.
\ No newline at end of file