From 5843163bd51a5f1a7310ffb64bda3b4c6bb50c0c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Apr 2021 11:23:55 +0200
Subject: [PATCH] Add TODO about `Z_mod_nonneg_nonneg`.

---
 theories/numbers.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/numbers.v b/theories/numbers.v
index e5a05b02..a08b7bf8 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1212,8 +1212,10 @@ Lemma rotate_nat_add_add_mod base offset len:
   rotate_nat_add base offset len =
   rotate_nat_add (Z.to_nat (base `mod` len)%Z) offset len.
 Proof.
-  unfold rotate_nat_add. rewrite !Z2Nat.id; [by rewrite Zplus_mod_idemp_l|].
-  destruct len as [|i]; [rewrite Zmod_0_r|apply Z_mod_lt]; lia.
+  (* TODO: [Z_mod_nonneg_nonneg] once that's part of all supported Coq versions *)
+  unfold rotate_nat_add. assert (0 ≤ base `mod` len)%Z.
+  { destruct len as [|i]; [rewrite Zmod_0_r|apply Z_mod_lt]; lia. }
+  by rewrite Z2Nat.id, Zplus_mod_idemp_l.
 Qed.
 
 Lemma rotate_nat_add_alt base offset len:
-- 
GitLab