diff options
Diffstat (limited to 'plugins/micromega/Fourier_util.v')
| -rw-r--r-- | plugins/micromega/Fourier_util.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/Fourier_util.v b/plugins/micromega/Fourier_util.v index b62153dee4..95fa5b88df 100644 --- a/plugins/micromega/Fourier_util.v +++ b/plugins/micromega/Fourier_util.v @@ -1,7 +1,7 @@ Require Export Rbase. Require Import Lra. -Open Scope R_scope. +Local Open Scope R_scope. Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. intros x y H H0; try assumption. |