proposition: Lemma Rmult_le_0_r : forall a b, a <= 0 -> 0 <= b -> a * b <= 0.
proof: Proof. intros ; rewrite <-(Rmult_0_r a) ; apply (Rmult_le_compat_neg_l a 0 b) with (1 := H) ; auto. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)