proposition: Lemma ler_rat : {mono (@ratr F) : x y / x <= y}.
proof: Proof. move=> x y /=; case: (ratP x) => nx dx cndx; case: (ratP y) => ny dy cndy. rewrite !fmorph_div /= !ratr_int !ler_pdivlMr ?ltr0z //. by rewrite ![_ / _ * _]mulrAC !ler_pdivrMr ?ltr0z // -!rmorphM /= !ler_int. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)