diff --git a/src/bbv/NatLib.v b/src/bbv/NatLib.v
index 1265446..9ffa06b 100644
--- a/src/bbv/NatLib.v
+++ b/src/bbv/NatLib.v
@@ -58,7 +58,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 auto with zarith; apply PH; intuition.
     exfalso; lia.
   Qed.
 
@@ -98,7 +98,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 lia.
 
   destruct k; simpl; intuition.
   rewrite <- plus_n_Sm.
@@ -374,7 +374,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 lia.
 Qed.
 
 Theorem pow2_N : forall n, Npow2 n = N.of_nat (pow2 n).
diff --git a/src/bbv/Nomega.v b/src/bbv/Nomega.v
index 98f0ccb..7065143 100644
--- a/src/bbv/Nomega.v
+++ b/src/bbv/Nomega.v
@@ -7,6 +7,8 @@ Require Import Coq.ZArith.ZArith.
 
 Local Open Scope N_scope.
 
+Local Ltac Tauto.intuition_solver ::= auto with bool zarith.
+
 Hint Rewrite Nplus_0_r nat_of_Nsucc nat_of_Nplus nat_of_Nminus
   N_of_nat_of_N nat_of_N_of_nat
   nat_of_P_o_P_of_succ_nat_eq_succ nat_of_P_succ_morphism : N.
diff --git a/src/bbv/Word.v b/src/bbv/Word.v
index 49f30d4..dedfa3e 100644
--- a/src/bbv/Word.v
+++ b/src/bbv/Word.v
@@ -531,7 +531,7 @@ 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 lia.
 Qed.
 
 Hint Rewrite roundTrip_0 : wordToNat.
@@ -539,7 +539,7 @@ 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 lia.
 
   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 lia.
 Qed.
 
 Lemma wordToNat_natToWord_2: forall sz w : nat,
@@ -5122,7 +5122,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 worder.
   rewrite wplus_wplusZ.
   unfold wplusZ, wordBinZ.
   destruct (wordToZ_ZToWord' (S sz) n) as [k1 D1].