diff --git a/stdpp/listZ.v b/stdpp/listZ.v
index 3c6bf20c508a02a735077a054482ddbd6768bafe..a5ec05ea46564de0783e13ad7832f8b75bb56f90 100644
--- a/stdpp/listZ.v
+++ b/stdpp/listZ.v
@@ -123,9 +123,9 @@ Lemma lookupZ_app l1 l2 i :
     match l1 !! i with Some x => Some x | None => l2 !! (i - lengthZ l1) end.
 Proof.
   rewrite !lookupZ_eq. Z.case_to_onat; simpl.
-  - rewrite lookup_app. case_match. 1:done.
+  - rewrite lookup_app. case_match eqn:Hli. 1:done.
     assert (lengthZ l1 ≤ i).
-    { rewrite lookup_ge_None in *. lia. }
+    { apply lookup_ge_None in Hli. lia. }
     rewrite Z.to_onat_nonneg by lia. simpl. f_equal. lia.
   - rewrite Z.to_onat_neg by lia. done.
 Qed.