From 72ba7f1418b61efa8e3f2cc547f941cd260f2f30 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Tue, 16 Apr 2024 22:33:33 -0400
Subject: [PATCH] Do not use Ndigits in NUtil (coq/coq #18936) (#1876)

---
 src/Util/NUtil.v | 41 -----------------------------------------
 1 file changed, 41 deletions(-)

diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
index b14356053e..56bd19017c 100644
--- a/src/Util/NUtil.v
+++ b/src/Util/NUtil.v
@@ -9,23 +9,6 @@ Require Import Crypto.Util.ZUtil.Z2Nat.
 Require Import Crypto.Util.ZUtil.Shift.
 
 Module N.
-  Lemma shiftr_size : forall n bound, N.size_nat n <= bound ->
-    N.shiftr_nat n bound = 0%N.
-  Proof.
-    intros n bound H.
-    rewrite <- (Nat2N.id bound).
-    rewrite Nshiftr_nat_equiv.
-    destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|].
-    apply N.shiftr_eq_0.
-    rewrite N.size_nat_equiv in *.
-    rewrite N.size_log2 in * by auto.
-    apply N.le_succ_l.
-    rewrite <- N.compare_le_iff.
-    rewrite N2Nat.inj_compare.
-    rewrite <- Compare_dec.nat_compare_le.
-    rewrite Nat2N.id.
-    auto.
-  Qed.
 
 #[global]
   Hint Rewrite
@@ -54,30 +37,6 @@ Module N.
     reflexivity.
   Qed.
 
-  Lemma shiftr_succ : forall n i,
-    N.to_nat (N.shiftr_nat n i) =
-    if N.testbit_nat n i
-    then S (2 * N.to_nat (N.shiftr_nat n (S i)))
-    else (2 * N.to_nat (N.shiftr_nat n (S i))).
-  Proof.
-    intros n i.
-    rewrite Nshiftr_nat_S.
-    case_eq (N.testbit_nat n i); intro testbit_i;
-      pose proof (Nshiftr_nat_spec n i 0) as shiftr_n_odd;
-      rewrite Nbit0_correct in shiftr_n_odd; simpl in shiftr_n_odd;
-      rewrite testbit_i in shiftr_n_odd.
-    + pose proof (Ndiv2_double_plus_one (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
-      rewrite succ_double_to_nat in Nsucc_double_shift.
-      apply Nat2N.inj.
-      rewrite Nsucc_double_shift.
-      apply N2Nat.id.
-    + pose proof (Ndiv2_double (N.shiftr_nat n i) shiftr_n_odd) as Nsucc_double_shift.
-      rewrite double_to_nat in Nsucc_double_shift.
-      apply Nat2N.inj.
-      rewrite Nsucc_double_shift.
-      apply N2Nat.id.
-  Qed.
-
   Section ZN.
     Import Coq.ZArith.ZArith.
     Lemma ZToN_NPow2_lt : forall z n, (0 <= z < 2 ^ Z.of_nat n)%Z ->