proposition: Lemma Rmult_le_compat_neg_r : forall r r1 r2 : R, (r <= 0)%R -> (r1 <= r2)%R -> (r2 * r <= r1 * r)%R.
proof: Proof. intros. rewrite (Rmult_comm r2). rewrite (Rmult_comm r1). apply Rmult_le_compat_neg_l. exact H. exact H0. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)