proposition: Theorem Rtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m.
proof: Proof. Proof (SORtimes_pos_pos sor). Theorem Rtimes_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n * m. Proof. intros n m H1 H2. le_elim H1. - le_elim H2. + le_less; now apply Rtimes_pos_pos. + rewrite <- H2; rewrite Rtimes_0_r; le_equal. - rewrite <- H1; rewrite Rtimes_0_l; le_equal. Qed.
imports: Setoid Ring