proposition: Lemma Rmult_neg_neg : forall r1 r2, r1 < 0 -> r2 < 0 -> r1 * r2 > 0.
proof: Proof. intros r1 r2 H1%Ropp_lt_contravar H2%Ropp_lt_contravar. rewrite Ropp_0 in H1, H2; rewrite <-Rmult_opp_opp. now apply Rmult_lt_0_compat. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField