proposition: Lemma approx_between s x1 x2 m1 m2 : approx s.+1 x1 m1 -> approx s.+1 x2 m2 -> 1 < exp2R s * (x2 - x1) -> exists2 m, (m1 + 1 <= m)%R & (m + 1 <= m2)%R.
proof: Proof. have [m] := approx_exists s (x1 + x2); rewrite /approx exp2RS. move: (exp2R s) => s2; set y := s2 * (x1 + x2); set z := s2 * (x2 - x1). have ->: 2 * s2 * x1 == y - z. by rewrite -mulRA mulRCA mul2R -mulRN -mulRDr oppRD addRA addRK oppRK. have ->: 2 * s2 * x2 == y + z. by rewrite -mulRA mulRCA -mulRDr (addRC (x1 + x2)) -addRA addKR mul2R. case=> Hmy Hym [Hm1 _] [_ Hm2] Hz. exists m; apply/(@intR_ltP R); rewrite -/intRR. apply: (leR_lt_trans Hm1); rewrite -(leR_add2r z) subRK. by apply: (ltR_trans Hym); rewrite leR_add2l. apply: (leR_lt_trans Hmy); rewrite -(leR_add2r z). by apply: (ltR_trans Hm2); rewrite leR_add2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple path fingraph bigop order ssralg) mathcomp(ssrnum ssrint div intdiv) fourcolor(hypermap geometry coloring grid matte) fourcolor(real realplane) Coq(Setoid Morphisms) fourcolor(realsyntax realprop)