1 files changed, 0 insertions, 32 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v
deleted file mode 100644
index 13847b50a..000000000
--- a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v
+++ /dev/null
@@ -1,32 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.LegacyArithmetic.Interface.
-Require Import Crypto.LegacyArithmetic.InterfaceProofs.
-Require Import Crypto.LegacyArithmetic.Double.Core.
-Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
-
-Local Open Scope Z_scope.
-Local Opaque tuple_decoder.
-Local Arguments Z.mul !_ !_.
-
-Section load_immediate.
-  Context {n W}
-          {decode : decoder n W}
-          {is_decode : is_decode decode}
-          {ldi : load_immediate W}
-          {is_ldi : is_load_immediate ldi}.
-
-  Global Instance is_load_immediate_double
-    : is_load_immediate (ldi_double n).
-  Proof using Type*.
-    intros x H; hnf in H.
-    pose proof (decode_exponent_nonnegative decode (ldi x)).
-    assert (0 <= x mod 2^n < 2^n) by auto with zarith.
-    assert (x / 2^n < 2^n)
-      by (apply Z.div_lt_upper_bound; autorewrite with pull_Zpow zsimplify; auto with zarith).
-    assert (0 <= x / 2^n < 2^n) by (split; Z.zero_bounds).
-    unfold ldi_double, load_immediate_double; simpl.
-    autorewrite with simpl_tuple_decoder Zshift_to_pow; simpl; push_decode.
-    autorewrite with zsimplify; reflexivity.
-  Qed.
-End load_immediate.