reduce imports

affeldt-aist · Jul 17, 2024 · 5d76686 · 5d76686
1 parent d0547a2
commit 5d76686
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.