proposition: Lemma Rdiv_neg_compat_rev (x y : R) : (x / y <= 0 -> 0 < y -> x <= 0)%R.
proof: Proof. intros Hx Hy. rewrite <-(@Rmult_0_l y), <-(@Rmult_1_r x). rewrite <-(Rinv_r y); [|now apply Rlt_neq_sym]. rewrite (Rmult_comm y), <-Rmult_assoc. apply Rmult_le_compat_r; trivial. now left. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux) Coquelicot.Coquelicot