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