proposition: Lemma ratR_leP a1 a2 : reflect (a1 <= a2) (a1 <= a2)%R.
proof: Proof. have [[r1 {3}-> Dr1] [r2 {3}-> Dr2]] := (ratR_eq a1, ratR_eq a2). rewrite ler_pdivl_mulr ?ltr0Sn // mulrAC ler_pdivr_mulr ?ltr0Sn //. rewrite -!intrM ler_int /=; apply: (equivP (intR_leP _ _)). by rewrite !intRM -Dr1 -Dr2 mulRAC !leR_pmul2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)