Adapt to rocq-prover/rocq#21129.

Author: ppedrot

src/bbv/NatLib.v

@@ -57,7 +57,7 @@ Section strong.
   Hypothesis PH : forall n, (forall m, m < n -> P m) -> P n.
 
   Lemma strong' : forall n m, m <= n -> P m.
-    induction n; simpl; intuition; apply PH; intuition.
+    induction n; simpl; intuition; apply PH; intuition; auto with *.
     exfalso; lia.
   Qed.
 
@@ -97,7 +97,7 @@ Theorem drop_mod2 : forall n k,
 
   do 2 (destruct n; simpl in *; repeat rewrite untimes2 in *; intuition).
 
-  destruct k; simpl in *; intuition.
+  destruct k; simpl in *; intuition; auto with *.
 
   destruct k; simpl; intuition.
   rewrite <- plus_n_Sm.
@@ -373,7 +373,7 @@ Qed.
 Theorem Npow2_nat : forall n, nat_of_N (Npow2 n) = pow2 n.
   induction n as [|n IHn]; simpl; intuition.
   rewrite <- IHn; clear IHn.
-  case_eq (Npow2 n); intuition; zify; intuition.
+  case_eq (Npow2 n); intuition; zify; intuition; auto with *.
 Qed.
 
 Theorem pow2_N : forall n, Npow2 n = N.of_nat (pow2 n).

src/bbv/Word.v

@@ -531,15 +531,15 @@ Theorem natToWord_wordToNat : forall sz w, natToWord sz (wordToNat w) = w.
 Qed.
 
 Theorem roundTrip_0 : forall sz, wordToNat (natToWord sz 0) = 0.
-  induction sz; simpl; intuition.
+  induction sz; simpl; intuition; auto with *.
 Qed.
 
 Hint Rewrite roundTrip_0 : wordToNat.
 
 Lemma wordToNat_natToWord' : forall sz w, exists k, wordToNat (natToWord sz w) + k * pow2 sz = w.
   induction sz as [|sz IHsz]; simpl; intro w; intuition; repeat rewrite untimes2.
 
-  exists w; intuition.
+  exists w; intuition; auto with *.
 
   case_eq (mod2 w); intro Hmw.
 
@@ -573,7 +573,7 @@ Qed.
 Theorem wordToNat_natToWord:
   forall sz w, exists k, wordToNat (natToWord sz w) = w - k * pow2 sz /\ (k * pow2 sz <= w)%nat.
 Proof.
-  intros sz w; destruct (wordToNat_natToWord' sz w) as [k]; exists k; intuition.
+  intros sz w; destruct (wordToNat_natToWord' sz w) as [k]; exists k; intuition; auto with *.
 Qed.
 
 Lemma wordToNat_natToWord_2: forall sz w : nat,
@@ -5125,7 +5125,7 @@ Qed.
 
 Lemma ZToWord_plus: forall sz a b, ZToWord sz (a + b) = ZToWord sz a ^+ ZToWord sz b.
 Proof.
-  destruct sz as [|sz]; intros n m; intuition.
+  destruct sz as [|sz]; intros n m; intuition; auto with *.
   rewrite wplus_wplusZ.
   unfold wplusZ, wordBinZ.
   destruct (wordToZ_ZToWord' (S sz) n) as [k1 D1].