Library Coq.micromega.Fourier_util
Require Export Rbase.
Require Import Lra.
Local Open Scope R_scope.
Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x.
Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
Require Import Lra.
Local Open Scope R_scope.
Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x.
Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.