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