diff --git a/probability/proba_mcreal.v b/probability/proba_mcreal.v
index 7426c79d..6eaf7f63 100644
--- a/probability/proba_mcreal.v
+++ b/probability/proba_mcreal.v
@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
 From mathcomp Require boolp.
 From mathcomp Require Import Rstruct reals.
-Require Import Reals Lra.
+Require Import Reals.
 Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext.
 Require Import bigop_ext fdist proba.