proposition: Lemma Rmult_le_pos_neg : forall x y : R, (0 <= x)%R -> (y <= 0)%R -> (x * y <= 0)%R.
proof: Proof. intros. rewrite <- (Rmult_0_r x). apply Rmult_le_compat_l ; assumption. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)