proposition: Lemma ratRMn a n : (a * n%:Q)%R == a * n.
proof: Proof. have [[r1 Da Dr1] [r2 Dan Dr2]] := (ratR_eq a, ratR_eq (a * n%:Q)). apply/(pmulIR (ltR0Sn r2.2))/(pmulIR (ltR0Sn r1.2)). rewrite {}Dr2 -2!(mulRAC _ r1.2.+1) {}Dr1 -!intRM -!ratRz !intrM. apply/eqR_congr/(congr1 ratRR)/(canRL (divfK _)); first by rewrite intr_eq0. by rewrite mulrAC -{}Dan {}Da mulrAC divfK ?intr_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)