proposition: Lemma rect_approx s z p (b_p : srect := (s, ltouch p)) : approx_point s z p -> exists2 r : rectangle, r z & subregion r b_p.
proof: Proof. case: z p => x y [mx my] in b_p * => -[[lbx ubx] [lby uby]]. have sXgt0: exp2R s > 0 by apply: ltR0exp2. have sZK u: exp2R s * (u / exp2R s) == u by rewrite [u / _]mulRC mulRCA pmulKR. pose step (m : int) := Interval ((m - 1)%R / exp2R s) ((m + 1)%R / exp2R s). exists (Rectangle (step mx) (step my)) => [|[x1 y1] [[]]]. split; split; rewrite -(leR_pmul2l _ _ sXgt0) sZK /intRR ?intRD1 //. by apply: ltR_le_trans lbx; apply/intR_ltP; rewrite subrK. by apply: ltR_le_trans lby; apply/intR_ltP; rewrite subrK. rewrite -(leR_pmul2l _ x1 sXgt0) -(leR_pmul2l x1 _ sXgt0) !sZK => lbx1 ubx1 []. rewrite -(leR_pmul2l _ y1 sXgt0) -(leR_pmul2l y1 _ sXgt0) !sZK => lby1 uby1. have [p1 Dp1] := approx_point_exists s (Point x1 y1); exists p1 => //. case: p1 Dp1 => [p1x p1y] [[ubp1x lbp1x] [ubp1y lbp1y]] /=. rewrite -!(rwP andP) -!ltz_addr1 -!lez_addr1 -!(rwP (@intR_ltP R _ _)). rewrite (intRD1 R p1x) (intRD1 R p1y) -/intRR; split. by split; [apply: ltR_trans lbp1x | apply: leR_lt_trans ubx1]. by split; [apply: ltR_trans lbp1y | apply: leR_lt_trans uby1]. 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)