proposition: Lemma intRB m1 m2 : (m1 - m2)%R == m1 - m2.
proof: Proof. by rewrite intRD intRN. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)