proposition: Lemma Rdiv_Rmult_neg_pos_Rle': forall x y z t, z<0 -> 0<t -> x / z <= y / t -> z*y <= t*x.
proof: Proof. intros x y z t Hz Ht Hxyzt; stepl ((z*t)*(y/t)); [|field; auto]; stepr ((z*t)*(x/z)); [|field; auto]; apply Rmult_le_compat_neg_l; auto; apply Rlt_le; auto; apply Rlt_mult_pos_neg; assumption. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)