proposition: Fact subq_ge0 x y : le_rat 0 (y - x) = le_rat x y.
proof: Proof. symmetry; rewrite ge_rat0 !le_ratE -subr_ge0. case: ratP => nx dx cndx; case: ratP => ny dy cndy. rewrite -!mulNr addf_div ?intq_eq0 // !mulNr -!rmorphM -rmorphB /=. symmetry; rewrite !leNgt -sgr_cp0 sgr_numq_div mulrC gtr0_sg //. by rewrite mul1r sgr_cp0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)