proposition: Lemma intRD m1 m2 : (m1 + m2)%R == m1 + m2.
proof: Proof. suffices intRDn m n: (m + n)%R == m + n. by case: m2 => // n; rewrite -[m1]opprK NegzE -opprD !(intRN, intRDn) oppRD. elim: n => [|n IHn]; first by rewrite addr0 addR0. by rewrite -addn1 PoszD addrA !intRD1 IHn addRA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)