Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

1 files changed, 31 insertions, 0 deletions

diff --git a/plugins/micromega/Fourier_util.v b/plugins/micromega/Fourier_util.v
new file mode 100644
index 00000000..b62153de
--- /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.