proposition: Lemma ratRD a1 a2 : (a1 + a2)%R == a1 + a2.
proof: Proof. have [[r1 {2}-> Dr1] [r2 {2}-> Dr2]] := (ratR_eq a1, ratR_eq a2). apply/(pmulIR (ltR0Sn r2.2))/(pmulIR (ltR0Sn r1.2)). rewrite !mulRDl (mulRAC a1) Dr1 Dr2 -!ratRMn !mulrDl mulrAC !divfK ?intr_eq0 //. by rewrite -!intrM -intrD ratRz intRD !intRM. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)