proposition: Fact le_rat0M x y : le_rat 0 x -> le_rat 0 y -> le_rat 0 (x * y).
proof: Proof. rewrite !ge_rat0 => hnx hny. have hxy: (0 <= numq x * denq y + numq y * denq x). by rewrite addr_ge0 ?mulr_ge0. rewrite [_ * _]mulq_def /numq /= -!/(denq _) ?mulf_eq0 ?denq_eq0. rewrite val_fracq/=; case: ifP => //=. by rewrite ?mulq_subdefE !mulr_ge0// !le_gtF ?mulr_ge0 ?denq_ge0//=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)