diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/fourier/Fourier_util.v | 2 | ||||
| -rw-r--r-- | contrib/fourier/fourierR.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/fourier/Fourier_util.v b/contrib/fourier/Fourier_util.v index e81fdb84e..c592af09a 100644 --- a/contrib/fourier/Fourier_util.v +++ b/contrib/fourier/Fourier_util.v @@ -152,7 +152,7 @@ apply Rlt_irrefl. ring. Qed. -Lemma Rlt_not_le : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d. +Lemma Rlt_not_le_frac_opp : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d. intros n d H; try assumption. apply Rgt_not_le. replace 0 with (-0). diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 8a3307f9d..d415cf7d2 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -334,7 +334,7 @@ let coq_Rfourier_le_lt = lazy (constant_fourier "Rfourier_le_lt") let coq_Rfourier_le_le = lazy (constant_fourier "Rfourier_le_le") let coq_Rnot_lt_lt = lazy (constant_fourier "Rnot_lt_lt") let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le") -let coq_Rlt_not_le = lazy (constant_fourier "Rlt_not_le") +let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp") (****************************************************************************** Construction de la preuve en cas de succès de la méthode de Fourier, @@ -404,7 +404,7 @@ let tac_zero_inf_false gl (n,d) = (* preuve que 0<=(-n)*(1/d) => False *) let tac_zero_infeq_false gl (n,d) = - (tclTHEN (apply (get coq_Rlt_not_le)) + (tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) (tac_zero_inf_pos gl (-n,d))) ;; |