proposition: Lemma Rmult_Rdiv_neg_Rlt: forall x y z t, (z < R0)%R -> (t < R0)%R -> (x * t < y * z)%R -> (x / z < y / t)%R.
proof: Proof. intros x y z t Hz Ht Hxtys; apply Rlt_zero_Rminus; rewrite Rminus_Rdiv; auto; unfold Rdiv; apply Fourier_util.Rlt_mult_inv_pos; auto; apply Rlt_Rminus_zero; assumption. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)