proposition: Lemma Rdiv_neg_compat (x y : R) : (x <= 0 -> 0 < y -> x / y <= 0)%R.
proof: Proof. intros Hx Hy. unfold Rdiv; rewrite <-(@Rmult_0_l (/ y)). apply Rmult_le_compat_r; trivial. now left; apply Rinv_0_lt_compat. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux) Coquelicot.Coquelicot