proposition: Lemma Rmult_pos_neg : forall r1 r2, r1 > 0 -> r2 < 0 -> r1 * r2 < 0.
proof: Proof. now intros r1 r2 H1 H2; rewrite Rmult_comm; apply Rmult_neg_pos. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField