diff --git a/src/Arithmetic/SolinasReduction.v b/src/Arithmetic/SolinasReduction.v
index 461c451fe0..07e8a94b77 100644
--- a/src/Arithmetic/SolinasReduction.v
+++ b/src/Arithmetic/SolinasReduction.v
@@ -10,7 +10,7 @@ Require Import Crypto.Arithmetic.ModOps.
 Require Import Crypto.Arithmetic.Partition.
 Require Import Crypto.Arithmetic.UniformWeight.
 Require Import Crypto.Arithmetic.Saturated.
-Require Coq.btauto.Btauto.
+Require Import (*hints*) Coq.btauto.Algebra.
 Require Coq.Structures.OrdersEx.
 Require Import Crypto.Util.ListUtil.StdlibCompat.
 Require Import Crypto.Util.ZUtil.ModInv.
diff --git a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v
index 29218bbe1c..f5c26ea960 100644
--- a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v
+++ b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.Bool.Bool.
 Require Import Coq.Lists.List.
 Require Import Coq.micromega.Lia.
+Require Import (*hints*) Coq.btauto.Algebra.
 Require Import bedrock2.Syntax.
 Require Import coqutil.Word.Interface coqutil.Word.Properties.
 Require Import coqutil.Map.Interface.
diff --git a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v
index 0052682dbf..e511e486d3 100644
--- a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v
+++ b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.Bool.Bool.
 Require Import Coq.Lists.List.
 Require Import Coq.micromega.Lia.
+Require Import (*hints*) Coq.btauto.Algebra.
 Require Import bedrock2.Syntax.
 Require Import coqutil.Word.Interface coqutil.Word.Properties.
 Require Import coqutil.Map.Interface.