From 2cb175e4ad44ac67a5754c9b28f670a4da3997a1 Mon Sep 17 00:00:00 2001
From: Jake Waksbaum <jake.waksbaum@gmail.com>
Date: Mon, 22 Apr 2019 01:21:05 -0400
Subject: [PATCH] Integers.v: add unsigned_inj

---
 lib/Integers.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/lib/Integers.v b/lib/Integers.v
index 4b75e71ede..2f8ed87c38 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -211,6 +211,21 @@ Definition one  := repr 1.
 Definition mone := repr (-1).
 Definition iwordsize := repr zwordsize.
 
+Lemma unsigned_inj : forall x y : int,
+    unsigned x = unsigned y -> x = y.
+Proof.
+  intros [xval Hxrange] [yal Hyrange] E.
+  cbn in E. subst.
+  replace Hxrange with Hyrange; [subst; reflexivity|].
+  destruct Hxrange; destruct Hyrange.
+  f_equal; apply eq_proofs_unicity;
+    intros [] [];
+      match goal with
+      | |- ?x = ?x \/ ?x <> ?x => left; reflexivity
+      | |- ?x = ?y \/ ?x <> ?y => right; intro c; inversion c
+      end.
+Qed.
+
 Lemma mkint_eq:
   forall x y Px Py, x = y -> mkint x Px = mkint y Py.
 Proof.