proposition: Lemma ratR_dense x y : x < y -> exists2 a : rat, x < a & a < y.
proof: Proof. move=> ltxy; pose z := y - x; have z_gt0: z > 0 by rewrite subR_le0. have [[d|n] [ledv ltvd1]] := find_range1z z^-1; last first. case: ltvd1; apply: ltRW; apply: leR_lt_trans (invR_gt0 z_gt0). by rewrite NegzE intRN intRS oppRD subRK -subR_ge0 add0R oppRK. set d1 : R := d.+1; have d1gt0: d1 > 0 by apply: ltR0Sn. have [m [lemx ltxm1]] := find_range1z (d1 * x). exists ((m + 1)%:Q / d.+1%:Q)%R; rewrite -(leR_pmul2r _ _ d1gt0) -ratRMn. by rewrite divfK ?intr_eq0 // mulRC ratRz intRD1. rewrite divfK ?intr_eq0 // ratRz intRD1. rewrite -(addKR x y) addRC -addRA -/z mulRC mulRDr -(divRR (gtR_neq z_gt0)). move: lemx; rewrite -(leR_add2r (d1 * z)); apply: ltR_le_trans. by rewrite leR_add2l mulRC leR_pmul2l // /d1 intRS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)