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