proposition: Lemma approx_rect z (r : rectangle) : r z -> exists2 b, inset_srect b z & subregion b r.
proof: Proof. case: z r => [x y] [[x0 x1] [y0 y1]] [[lbx ubx] [lby uby]]. pose i4 := @Ordinal 4; pose dxy := tnth [tuple x - x0; x1 - x; y - y0; y1 - y]. have{lbx ubx lby uby} [s scale_s_dxy]: exists s, forall i, 1 < exp2R s * dxy i. have dxy_gt0 i: 0 < dxy i by case: i; do 4?case=> [?|]; rewrite ?subR_le0. have /fin_all_exists[s lbs] i := scale_exists (dxy_gt0 i). exists (\max_i s i) => i. exact/(ltR_le_trans (lbs i))/leR_pmul2r/leRexp2/leq_bigmax. pose s1 := s.+1; pose ap_s1 := approx s1; have es1gt0 := ltR0exp2 s1. have [[mx Dmx] [my Dmy]] := (approx_exists s1 x, approx_exists s1 y). have [[mx0 Dmx0] [mx1 Dmx1]] := (approx_exists s1 x0, approx_exists s1 x1). have [[my0 Dmy0] [my1 Dmy1]] := (approx_exists s1 y0, approx_exists s1 y1). have [nx0 lbx0 ubx0] := approx_between Dmx0 Dmx (scale_s_dxy (i4 0%N isT)). have [nx1 lbx1 ubx1] := approx_between Dmx Dmx1 (scale_s_dxy (i4 1%N isT)). have [ny0 lby0 uby0] := approx_between Dmy0 Dmy (scale_s_dxy (i4 2%N isT)). have [ny1 lby1 uby1] := approx_between Dmy Dmy1 (scale_s_dxy (i4 3%N isT)). exists (s1, Grect nx0 (nx1 + 1) ny0 (ny1 + 1)) => /=. by exists (Gpoint mx my); rewrite //= !addrK -!lez_addr1 ubx0 lbx1 uby0 lby1. have lt_approx u v mu mv: ap_s1 u mu -> ap_s1 v mv -> (mu + 1 <= mv)%R -> u < v. case=> _ ubu [lbv _] ltuv; apply/(leR_pmul2l v u es1gt0)/(ltR_le_trans ubu). by apply: leR_trans lbv; rewrite -intRD1; apply/intR_leP. case=> x2 y2 [[mx2 my2] [Dmx2 Dmy2]] /=; rewrite -andbA -!lez_addr1 => /and4P[]. move=> /(le_trans lbx0)/lt_approx-lbx /le_trans/(_ ubx1)/lt_approx-ubx. move=> /(le_trans lby0)/lt_approx-lby /le_trans/(_ uby1)/lt_approx-uby. by do 2!split; [apply/lbx | apply/ubx | apply/lby | apply/uby]. 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)