diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
index aae5ff4a..25ee05e5 100644
--- a/Arm/Insts/Common.lean
+++ b/Arm/Insts/Common.lean
@@ -496,7 +496,7 @@ instance : ToString SIMDThreeSameLogicalType where toString a := toString (repr
 ----------------------------------------------------------------------
 
 @[state_simp_rules]
-def Vpart_read (n : BitVec 5) (part width : Nat) (s : ArmState) (H : width > 0)
+def Vpart_read (n : BitVec 5) (part width : Nat) (s : ArmState)
   : BitVec width :=
   -- assert n >= 0 && n <= 31;
   -- assert part IN {0, 1};
@@ -656,7 +656,7 @@ deriving DecidableEq, Repr
 export ShiftInfo (esize elements shift unsigned round accumulate)
 
 @[state_simp_rules]
-def RShr (unsigned : Bool) (value : Int) (shift : Nat) (round : Bool) (h : n > 0)
+def RShr (unsigned : Bool) (value : Int) (shift : Nat) (round : Bool)
   : BitVec n :=
   -- assert shift > 0
   let fn := if unsigned then ushiftRight else sshiftRight
@@ -679,7 +679,7 @@ def shift_right_common_aux
     result
   else
     let elem := Int_with_unsigned info.unsigned $ elem_get operand e info.esize
-    let shift_elem := RShr info.unsigned elem info.shift info.round info.h
+    let shift_elem := RShr info.unsigned elem info.shift info.round
     let acc_elem := elem_get operand2 e info.esize + shift_elem
     let result := elem_set result e info.esize acc_elem info.h
     have _ : info.elements - (e + 1) < info.elements - e := by omega
diff --git a/Arm/Insts/DPSFP/Advanced_simd_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_copy.lean
index a9c2b35b..ffd077a1 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_copy.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_copy.lean
@@ -117,7 +117,6 @@ def exec_smov_umov (inst : Advanced_simd_copy_cls) (s : ArmState) (signed : Bool
     let idxdsize := 64 <<< (lsb inst.imm5 4).toNat
     -- if index == 0 then CheckFPEnabled64 else CheckFPAdvSIMDEnabled64
     let operand := read_sfp idxdsize inst.Rn s
-    have h₀ : esize > 0 := by apply zero_lt_shift_left_pos (by decide)
     let element := elem_get operand index esize
     let result := if signed then signExtend datasize element else zeroExtend datasize element
     -- State Updates
diff --git a/Arm/Insts/DPSFP/Advanced_simd_extract.lean b/Arm/Insts/DPSFP/Advanced_simd_extract.lean
index ce48a09d..9ec571cd 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_extract.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_extract.lean
@@ -32,10 +32,6 @@ def exec_advanced_simd_extract
     let lo := read_sfp datasize inst.Rn s
     let concat := hi ++ lo
     let result := extractLsb' position datasize concat
-    have h_datasize : 1 <= datasize := by simp_all! [datasize]; split <;> decide
-    have h : (position + datasize - 1 - position + 1) = datasize := by
-      rw [Nat.add_sub_assoc, Nat.add_sub_self_left]
-      exact Nat.sub_add_cancel h_datasize; trivial
     let s := write_sfp datasize inst.Rd result s
     let s := write_pc ((read_pc s) + 4#64) s
     s
diff --git a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean
index a28b8c99..47a1c98d 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean
@@ -27,7 +27,6 @@ def exec_advanced_simd_scalar_copy
     let idxdsize := 64 <<< (lsb inst.imm5 4).toNat
     let esize := 8 <<< size
     let operand := read_sfp idxdsize inst.Rn s
-    have h : esize > 0 := by apply zero_lt_shift_left_pos (by decide)
     let result := elem_get operand index.toNat esize
     -- State Updates
     let s := write_pc ((read_pc s) + 4#64) s
diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean
index 5a64fe3f..87dede23 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean
@@ -58,9 +58,8 @@ def exec_pmull (inst : Advanced_simd_three_different_cls) (s : ArmState) : ArmSt
     let datasize := 64
     let part := inst.Q.toNat
     let elements := datasize / esize
-    have h₁ : datasize > 0 := by decide
-    let operand1 := Vpart_read inst.Rn part datasize s h₁
-    let operand2 := Vpart_read inst.Rm part datasize s h₁
+    let operand1 := Vpart_read inst.Rn part datasize s
+    let operand2 := Vpart_read inst.Rm part datasize s
     let result :=
       pmull_op 0 esize elements operand1 operand2 (BitVec.zero (2*datasize)) h₀
     let s := write_sfp (datasize*2) inst.Rd result s
diff --git a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean
index 6e86c85c..b1f60918 100644
--- a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean
+++ b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean
@@ -19,12 +19,11 @@ open BitVec
 @[state_simp_rules]
 def fmov_general_aux (intsize : Nat) (fltsize : Nat) (op : FPConvOp)
   (part : Nat) (inst : Conversion_between_FP_and_Int_cls) (s : ArmState)
-  (H : 0 < fltsize)
   : ArmState :=
   -- Assume CheckFPEnabled64()
   match op with
   | FPConvOp.FPConvOp_MOV_FtoI =>
-    let fltval := Vpart_read inst.Rn part fltsize s H
+    let fltval := Vpart_read inst.Rn part fltsize s
     let intval := zeroExtend intsize fltval
     -- State Update
     let s := write_gpr intsize inst.Rd intval s
@@ -44,12 +43,6 @@ def exec_fmov_general
   (inst : Conversion_between_FP_and_Int_cls) (s : ArmState): ArmState :=
   let intsize := 32 <<< inst.sf.toNat
   let decode_fltsize := if inst.ftype = 0b10#2 then 64 else (8 <<< (inst.ftype ^^^ 0b10#2).toNat)
-  have H: 0 < decode_fltsize := by
-    simp only [decode_fltsize, beq_iff_eq]
-    split
-    · decide
-    · generalize BitVec.toNat (inst.ftype ^^^ 2#2) = x
-      apply zero_lt_shift_left_pos (by decide)
   match (extractLsb' 1 2 inst.opcode) ++ inst.rmode with
   | 1100 =>  -- FMOV
     if decode_fltsize ≠ 16 ∧ decode_fltsize ≠ intsize then
@@ -59,7 +52,7 @@ def exec_fmov_general
                 then FPConvOp.FPConvOp_MOV_ItoF
                 else FPConvOp.FPConvOp_MOV_FtoI
       let part := 0
-      fmov_general_aux intsize decode_fltsize op part inst s H
+      fmov_general_aux intsize decode_fltsize op part inst s
   | 1101 => -- FMOV D[1]
     if intsize ≠ 64 ∨ inst.ftype ≠ 0b10#2 then
       write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
@@ -68,7 +61,7 @@ def exec_fmov_general
                 then FPConvOp.FPConvOp_MOV_ItoF
                 else FPConvOp.FPConvOp_MOV_FtoI
       let part := 1
-      fmov_general_aux intsize decode_fltsize op part inst s H
+      fmov_general_aux intsize decode_fltsize op part inst s
     | _ => write_err (StateError.Other s!"exec_fmov_general called with non-FMOV instructions!") s
 
 @[state_simp_rules]
diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean
index 6c9b1493..e58e3f73 100644
--- a/Arm/Insts/DPSFP/Crypto_aes.lean
+++ b/Arm/Insts/DPSFP/Crypto_aes.lean
@@ -52,7 +52,6 @@ def FFmul02 (b : BitVec 8) : BitVec 8 :=
       0x1E1C1A18161412100E0C0A0806040200#128  -- 0
     ]
   let lo := b.toNat * 8
-  let hi := lo + 7
   extractLsb' lo 8 $ BitVec.flatten FFmul_02
 
 def FFmul03 (b : BitVec 8) : BitVec 8 :=
diff --git a/Arm/Insts/LDST/Reg_pair.lean b/Arm/Insts/LDST/Reg_pair.lean
index b962eb09..5c0c6263 100644
--- a/Arm/Insts/LDST/Reg_pair.lean
+++ b/Arm/Insts/LDST/Reg_pair.lean
@@ -40,7 +40,7 @@ def reg_pair_constrain_unpredictable (wback : Bool) (inst : Reg_pair_cls) : Bool
 @[state_simp_rules]
 def reg_pair_operation (inst : Reg_pair_cls) (inst_str : String) (signed : Bool)
   (datasize : Nat) (offset : BitVec 64) (s : ArmState)
-  (H1 : 8 ∣ datasize) (H2 : 0 < datasize) : ArmState :=
+  (H1 : 8 ∣ datasize): ArmState :=
   -- Note: we do not need to model the ASL function
   -- "CreateAccDescGPR" here, given the simplicity of our memory
   -- model
@@ -99,11 +99,8 @@ def exec_reg_pair_common (inst : Reg_pair_cls) (inst_str : String) (s : ArmState
     let offset := (signExtend 64 inst.imm7) <<< scale
     have H1 : 8 ∣ datasize := by
       simp_all! only [gt_iff_lt, Nat.shiftLeft_eq, Nat.dvd_mul_right, datasize]
-    have H2 : 0 < datasize := by
-      simp_all! only [datasize]
-      apply zero_lt_shift_left_pos (by decide)
     -- State Updates
-    let s' := reg_pair_operation inst inst_str signed datasize offset s H1 H2
+    let s' := reg_pair_operation inst inst_str signed datasize offset s H1
     let s' := write_pc ((read_pc s) + 4#64) s'
     s'
 
diff --git a/Specs/GCM.lean b/Specs/GCM.lean
index 17915aa4..b7496b62 100644
--- a/Specs/GCM.lean
+++ b/Specs/GCM.lean
@@ -22,7 +22,7 @@ def R : (BitVec 128) := 0b11100001#8 ++ 0b0#120
 abbrev Cipher {n : Nat} {m : Nat} :=  BitVec n → BitVec m → BitVec n
 
 /-- The s-bit incrementing function -/
-def inc_s (s : Nat) (X : BitVec l) (H₀ : 0 < s) (H₁ : s < l) : BitVec l :=
+def inc_s (s : Nat) (X : BitVec l) (H₀ : s < l) : BitVec l :=
   let upper := extractLsb' s (l - s) X
   let lower := (extractLsb' 0 s X) + 0b1#s
   have h : l - s + s = l := by omega
@@ -72,7 +72,7 @@ def GCTR_aux (CIPH : Cipher (n := 128) (m := m))
     let Xi := extractLsb' lo 128 X
     let Yi := Xi ^^^ CIPH ICB K
     let Y := BitVec.partInstall hi lo (BitVec.cast h Yi) Y
-    let ICB := inc_s 32 ICB (by omega) (by omega)
+    let ICB := inc_s 32 ICB (by omega)
     GCTR_aux CIPH (i + 1) n K ICB X Y
   termination_by (n - i)
 
@@ -130,7 +130,7 @@ def GCM_AE (CIPH : Cipher (n := 128) (m := m))
   : (BitVec p) × (BitVec t) :=
   let H := CIPH (BitVec.zero 128) K
   let J0 : BitVec 128 := GCM.initialize_J0 H IV
-  let ICB := inc_s 32 J0 (by decide) (by decide)
+  let ICB := inc_s 32 J0 (by decide)
   let C := GCTR (m := m) CIPH K ICB P
   let u := GCM.ceiling_in_bits p - p
   let v := GCM.ceiling_in_bits a - a
@@ -165,7 +165,7 @@ def GCM_AD (CIPH : Cipher (n := 128) (m := m))
   else
     let H := CIPH (BitVec.zero 128) K
     let J0 := GCM.initialize_J0 H IV
-    let ICB := inc_s 32 J0 (by decide) (by decide)
+    let ICB := inc_s 32 J0 (by decide)
     let P := GCTR (m := m) CIPH K ICB C
     let u := GCM.ceiling_in_bits c - c
     let v := GCM.ceiling_in_bits a - a