From 2554d1030faa3e67929d93f07c8d127562c26b62 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Tue, 4 May 2021 16:03:05 +0200
Subject: [PATCH] rename conversion lemmas to follow convention

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

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 979737e6..556ea185 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -227,7 +227,7 @@ Section Z_little_endian.
     by rewrite !iter_nat_of_Z, Zabs2Nat.inj_succ by lia.
   Qed.
 
-  Lemma little_endian_to_Z_to_little_endian m n bs:
+  Lemma Z_to_little_endian_to_Z m n bs:
     m = Z.of_nat (length bs) → 0 ≤ n →
     Forall (λ b, 0 ≤ b < 2 ^ n) bs →
     Z_to_little_endian m n (little_endian_to_Z n bs) = bs.
@@ -249,7 +249,7 @@ Section Z_little_endian.
   Qed.
 
   (* TODO: replace the calls to [nia] by [lia] after dropping support for Coq 8.10.2. *)
-  Lemma Z_to_little_endian_to_Z m n z:
+  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.
-- 
GitLab