diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 948a98f18cf14feb75eff25c52dcfd67b1087f3f..dd67e296cd04726f326d043d9e21285ec7352b08 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -77,14 +77,8 @@ build-coq.8.12.2:
     DENY_WARNINGS: "1"
 
 build-coq.8.11.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.11.2"
-    DENY_WARNINGS: "1"
-
-build-coq.8.10.2:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.10.2"
+    OPAM_PINS: "coq version 8.11.2"
     DENY_WARNINGS: "1"
diff --git a/README.md b/README.md
index eeb23fba9d207bc185d07baea46f121f2264d4cf..be93cd60a1b4f39b31a97d74c15fdd27f1333f05 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,7 @@ Notably:
 
 This version is known to compile with:
 
- - Coq version 8.10.2 / 8.11.2 / 8.12.2 / 8.13.2 / 8.14.1
+ - Coq version 8.11.2 / 8.12.2 / 8.13.2 / 8.14.1
 
 ## Installing via opam
 
diff --git a/coq-stdpp.opam b/coq-stdpp.opam
index 67872a065c70ef50536c8479cbac46bd5033beb2..1e5f8d626ef442df7e03ee132337e03c85e6ac82 100644
--- a/coq-stdpp.opam
+++ b/coq-stdpp.opam
@@ -33,7 +33,7 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.10.2" & < "8.15~") | (= "dev") }
+  "coq" { (>= "8.11" & < "8.15~") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 5eab4ad96aae2865bd98a65baff874fd10e46ec3..6935137074870c2079f54f118e732bc618a1c24a 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -321,12 +321,11 @@ Section Z_little_endian.
       rewrite orb_false_l. f_equal. lia.
   Qed.
 
-  (* TODO: replace the calls to [nia] by [lia] after dropping support for Coq 8.10.2. *)
   Lemma little_endian_to_Z_to_little_endian m n z:
     0 ≤ n → 0 ≤ m →
     little_endian_to_Z n (Z_to_little_endian m n z) = z `mod` 2 ^ (m * n).
   Proof.
-    intros ? Hm. rewrite <-Z.land_ones by nia.
+    intros ? Hm. rewrite <-Z.land_ones by lia.
     revert z.
     induction m as [|m ? IH|] using (Z_succ_pred_induction 0); intros z; [..|lia].
     { Z.bitwise. by rewrite andb_false_r. }
@@ -335,10 +334,10 @@ Section Z_little_endian.
     rewrite Z.land_spec, Z.lor_spec, Z.shiftl_spec, !Z.land_spec by lia.
     rewrite (Z_ones_spec n z') by lia. case_bool_decide.
     - rewrite andb_true_r, (Z.testbit_neg_r _ (z' - n)), orb_false_r by lia. simpl.
-      by rewrite Z_ones_spec, bool_decide_true, andb_true_r by nia.
+      by rewrite Z_ones_spec, bool_decide_true, andb_true_r by lia.
     - rewrite andb_false_r, orb_false_l.
       rewrite Z.shiftr_spec by lia. f_equal; [f_equal; lia|].
-      rewrite !Z_ones_spec by nia. apply bool_decide_iff. lia.
+      rewrite !Z_ones_spec by lia. apply bool_decide_iff. lia.
   Qed.
 
   Lemma Z_to_little_endian_length m n z :
@@ -368,11 +367,11 @@ Section Z_little_endian.
     0 ≤ little_endian_to_Z n bs < 2 ^ (Z.of_nat (length bs) * n).
   Proof.
     intros ?. induction 1 as [|b bs Hb ? IH]; [done|]; simpl.
-    apply Z_bounded_iff_bits_nonneg'; [nia|..].
+    apply Z_bounded_iff_bits_nonneg'; [lia|..].
     { apply Z.lor_nonneg. split; [lia|]. apply Z.shiftl_nonneg. lia. }
     intros z' ?. rewrite Z.lor_spec.
     rewrite Z_bounded_iff_bits_nonneg' in Hb by lia.
-    rewrite Hb, orb_false_l, Z.shiftl_spec by nia.
-    apply (Z_bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); nia.
+    rewrite Hb, orb_false_l, Z.shiftl_spec by lia.
+    apply (Z_bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); lia.
   Qed.
 End Z_little_endian.