proposition: Lemma ratR_ltP a1 a2 : reflect (a1 < a2) (a1 < a2)%R.
proof: Proof. by rewrite ltNge; apply: (iffP idP) => /ratR_leP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)