proposition: Lemma intR_leP m1 m2 : reflect (m1 <= m2) (m1 <= m2)%R.
proof: Proof. apply: (equivP idP); rewrite -subr_ge0 -subR_ge0 -intRB. by case: (m2 - m1)%R => n; split; rewrite // -oppR0 leR_opp2 => /ltR0Sn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)