diff --git a/doc/changelog/01-changed/258-bits-skipn-app.rst b/doc/changelog/01-changed/258-bits-skipn-app.rst
new file mode 100644
index 0000000000..ee30de8857
--- /dev/null
+++ b/doc/changelog/01-changed/258-bits-skipn-app.rst
@@ -0,0 +1,7 @@
+- in `theories/Zmod/Bits.v`
+
+  + Fixed lemma `bits.skipn_app` to actually describe the interaction between
+    the titular functions. Developments relying on the previous tautological
+    statement can resore it by adding that version of the lemma to the codebase
+    (`#258 <https://github.com/coq/stdlib/pull/258>`_,
+    by Andres Erbsen).
diff --git a/theories/Zmod/Bits.v b/theories/Zmod/Bits.v
index 1fd29043ff..0795e0cf12 100644
--- a/theories/Zmod/Bits.v
+++ b/theories/Zmod/Bits.v
@@ -415,11 +415,11 @@ Proof.
 Qed.
 
 Lemma skipn_app [n m] a b (Hn : 0 <= n) (Hm : 0 <= m) :
-  skipn n (@app n m a b) = of_Z _ (to_Z (skipn n (@app n m a b))).
+  skipn n (@app n m a b) = of_Z _ (to_Z b).
 Proof.
   case (skipn_app_ex a b) as [?->]; trivial.
-  apply to_Z_inj; rewrite to_Z_eq_rect, to_Z_of_Z.
-  rewrite Z.add_simpl_l, mod_to_Z; trivial.
+  apply to_Z_inj. rewrite to_Z_eq_rect, to_Z_of_Z.
+  pose proof unsigned_range b. rewrite Z.mod_small; lia.
 Qed.
 
 Lemma app_assoc_dep [n m l] (a : bits n) (b : bits m) (c : bits l)