proposition: Theorem Rtimes_neg_neg : forall n m : R, n < 0 -> m < 0 -> 0 < n * m.
proof: Proof. intros n m H1 H2. setoid_replace (n * m) with ((- n) * (- m)) by ring. apply Rtimes_pos_pos; now apply <- Ropp_pos_neg. Qed.
imports: Setoid Ring