proposition: Lemma intRD1 m : (m + 1)%R == m + 1.
proof: Proof. case: m => [n|[|n]]; [by rewrite addrC intRS | by rewrite addRC subRR |]. by rewrite /= subn1 oppRD subRK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)