diff --git a/complete_dioid.v b/complete_dioid.v
index af5ae77..fd6c252 100644
--- a/complete_dioid.v
+++ b/complete_dioid.v
@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice order.
 From mathcomp Require Import fintype ssrnat bigop.
+Require Import mathcomp.analysis.boolp.
 Require Import mathcomp.analysis.classical_sets.
 Require Import HB_wrappers dioid complete_lattice.