From 47459bd152dcee8dbd457171ac1cb8554079e739 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@gmail.com>
Date: Tue, 28 Nov 2023 11:26:43 -0600
Subject: [PATCH] Fix one warning

---
 src/Function.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Function.v b/src/Function.v
index 8e73ed6..4ffee6b 100644
--- a/src/Function.v
+++ b/src/Function.v
@@ -1,4 +1,4 @@
-Require Import Recdef Div2 Lia FunctionalExtensionality.
+From Coq Require Import PeanoNat Recdef Lia FunctionalExtensionality.
 
 (** Counting the number of digits in binary representation. *)
 
@@ -17,7 +17,7 @@ Function attempt_2 (n r : nat) {measure (fun x => x) n} : nat :=
   | _ => attempt_2 (Nat.div2 n) (r + 1)
   end.
 Proof.
-  intros. apply lt_div2. lia.
+  intros. apply Nat.lt_div2. lia.
 Defined.
 
 Compute attempt_2 1024 0.
@@ -29,7 +29,7 @@ Function attempt_3 (n r : nat) {wf lt n} : nat :=
   | _ => attempt_3 (Nat.div2 n) (r + 1)
   end.
 Proof.
-  + intros. apply lt_div2. lia.
+  + intros. apply Nat.lt_div2. lia.
   + apply Wf_nat.lt_wf.
 Defined.
 
@@ -90,7 +90,7 @@ Lemma div2_smaller : forall n n',
 Proof.
   destruct n; intros.
   discriminate.
-  apply lt_div2; lia.
+  apply Nat.lt_div2; lia.
 Qed.
 
 Definition numdigits (n: nat) : nat.