proposition: Lemma Rmult_Rdiv_neg_Rle: 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 Rle_zero_Rminus; rewrite Rminus_Rdiv; auto; unfold Rdiv; apply Rle_mult_inv_pos; auto; apply Rle_Rminus_zero; assumption. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)