diff --git a/stdpp_unstable/bitvector_tactics.v b/stdpp_unstable/bitvector_tactics.v
index 4efcc067358d322782a56282664b563a3938c40e..e3c2dfc0c3279b224bbd60c869f714ef55fadf0a 100644
--- a/stdpp_unstable/bitvector_tactics.v
+++ b/stdpp_unstable/bitvector_tactics.v
@@ -482,14 +482,22 @@ Tactic Notation "bv_simplify" :=
   with length of lists of bytes. *)
   reduce_closed_N;
   autorewrite with bv_simplify;
-  first [apply bv_eq_wrap | apply bv_neq_wrap | idtac];
+  lazymatch goal with
+  | |- _ =@{bv _} _ => apply bv_eq_wrap
+  | |- not (_ =@{bv _} _) => apply bv_neq_wrap
+  | _ => idtac
+  end;
   bv_unfold;
   autorewrite with bv_unfolded_simplify.
 
 Tactic Notation "bv_simplify" ident(H) :=
   unfold_lets_in_context;
   autorewrite with bv_simplify in H;
-  first [ apply bv_eq in H | apply bv_neq in H | idtac ];
+  lazymatch (type of H) with
+  | _ =@{bv _} _ => apply bv_eq in H
+  | not (_ =@{bv _} _) => apply bv_neq in H
+  | _ => idtac
+  end;
   tactic bv_unfold in H;
   autorewrite with bv_unfolded_simplify in H.
 Tactic Notation "bv_simplify" "select" open_constr(pat) :=
diff --git a/tests/bitvector_tactics.ref b/tests/bitvector_tactics.ref
index cb9e104d779e226257918ae9df0cca54c040b91d..49555584cac3c700e5a65e3c00437aa339870767 100644
--- a/tests/bitvector_tactics.ref
+++ b/tests/bitvector_tactics.ref
@@ -64,3 +64,25 @@ goal 2 is:
        (bv_wrap (16 * 2) (bv_unsigned v ≫ Z.of_N (16 * 2)) ≪ Z.of_N (16 * 2))
        (Z.lor (bv_unsigned b ≪ Z.of_N (16 * 1))
           (bv_wrap (16 * 1) (bv_unsigned v))))
+1 goal
+  
+  b : bv 16
+  ============================
+  bv_wrap 16 (bv_unsigned b) = bv_wrap 16 (bv_unsigned b)
+1 goal
+  
+  b : bv 16
+  ============================
+  bv_wrap 16 (bv_unsigned b) ≠ bv_wrap 16 (bv_unsigned b + 1)
+1 goal
+  
+  b : bv 16
+  H : bv_unsigned b = bv_unsigned b
+  ============================
+  True
+1 goal
+  
+  b : bv 16
+  H : bv_unsigned b ≠ bv_wrap 16 (bv_unsigned b + 1)
+  ============================
+  True
diff --git a/tests/bitvector_tactics.v b/tests/bitvector_tactics.v
index b5b2f6f50b8b48f218b9b52490a2d3bdc269a4fb..149be4f83f75610153458b14a814b1a443020041 100644
--- a/tests/bitvector_tactics.v
+++ b/tests/bitvector_tactics.v
@@ -73,3 +73,13 @@ Goal ∀ b : bv 16, ∀ v : bv 64,
 Proof.
   intros. bv_simplify. Show. bitblast.
 Qed.
+
+(** Regression test for https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/411 *)
+Goal ∀ b : bv 16, bv_wrap 16 (bv_unsigned b) = bv_wrap 16 (bv_unsigned b).
+Proof. intros. bv_simplify. Show. Restart. intros. bv_solve. Qed.
+Goal ∀ b : bv 16, bv_wrap 16 (bv_unsigned b) ≠ bv_wrap 16 (bv_unsigned (b + BV 16 1)).
+Proof. intros. bv_simplify. Show. Restart. intros. bv_solve. Qed.
+Goal ∀ b : bv 16, bv_unsigned b = bv_unsigned b → True.
+Proof. intros ? H. bv_simplify H. Show. Abort.
+Goal ∀ b : bv 16, bv_unsigned b ≠ bv_unsigned (b + BV 16 1) → True.
+Proof. intros ? H. bv_simplify H. Show. Abort.