Merge PR #7897: Remove fourier plugin

2 files changed, 36 insertions, 0 deletions

diff --git a/plugins/micromega/Fourier.v b/plugins/micromega/Fourier.v
new file mode 100644
index 000000000..0153de1da
--- /dev/null
+++ b/plugins/micromega/Fourier.v
@@ -0,0 +1,5 @@
+Require Import Lra.
+Require Export Fourier_util.
+
+#[deprecated(since = "8.9.0", note = "Use lra instead.")]
+Ltac fourier := lra.
diff --git a/plugins/micromega/Fourier_util.v b/plugins/micromega/Fourier_util.v
new file mode 100644
index 000000000..b62153dee
--- /dev/null
+++ b/plugins/micromega/Fourier_util.v
@@ -0,0 +1,31 @@
+Require Export Rbase.
+Require Import Lra.
+
+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.
+replace 0 with (x * 0).
+apply Rmult_lt_compat_l; auto with real.
+ring.
+Qed.
+
+Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x.
+intros x H; try assumption.
+rewrite Rplus_comm.
+apply Rle_lt_0_plus_1.
+red; auto with real.
+Qed.
+
+Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
+  intros; lra.
+Qed.
+
+Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
+intros x y H H0; try assumption.
+case H; intros.
+red; left.
+apply Rlt_mult_inv_pos; auto with real.
+rewrite <- H1.
+red; right; ring.
+Qed.