proposition: Lemma discretize_to_hypermap : exists2 G, planar_bridgeless G & four_colorable G -> colorable_with 4 m0.
proof: Proof. have m0tr_cl z t: m0 z t -> subregion (closure (m0 t)) (closure (m0 z)). by move=> m0zt u t_u U openU /t_u[] // v [/(m0tr m0zt)]; exists v. have [Nr [mr mrP mr_m0]] := exists_map_repr. have [ab [abP [s ab_mrP]] ab_m0] := exists_adjbox mrP. have [s1 [cm cmP]] := exists_smatte mrP ab_mrP. without loss Ds1: s s1 ab cm abP ab_mrP ab_m0 cmP / s1 = s. pose s2 := s + s1; pose ab2 e := (refine_srect s1 (s, ab e) : srect).2. move/(_ s2 s2 ab2 (fun i => (refine_smatte s (s1, cm i) : smatte).2)). apply=> // [||e [m0ij ltij]|i]. - rewrite /ab2; elim: (s1) => //= n IHn => e f p. by rewrite !in_refine_rect; apply: IHn. - by rewrite [s2]addnC => e i; apply/ab_mr_proper_refine/ab_mrP. - by rewrite gr_proper_refine ab_m0. apply: refine_smatte_proper (s1, _) _ _ _. have [m0i_cm cmi_ab] := cmP i; split=> // e /cmi_ab-cmi_e. rewrite gr_proper_refine => /cmi_e[z [mi_z ab_z]]; rewrite [s2]addnC. by exists z; split; last apply/in_refine_inset: ab_z. have{ab_mrP} ab_cmP e i: ab_cm_proper ab cm e i. move=> ab_e; have [m0i_cm e_cmi] := cmP i. split=> [/e_cmi[] // z [[p Dp cm_p] [q Dq ab_q]] | /hasP[p ab_p cmi_p]]. by apply/hasP; exists q; rewrite // -[q](approx_point_inj Dp) ?Ds1. have [_ ->//] := ab_mrP e i ab_e; exists (scale_point R s p). by split; last apply/m0i_cm; rewrite -Ds1; apply/mem_approx_scale. have {}cmP: cm_proper cm. move=> i j /hasP[p /= cmi_p cmj_p]. have [_ /(_ j)-> //] := mrP i; apply: m0tr (scale_point R s1 p) _ _ _. by have [m0_cmi _] := cmP i; apply/m0_cmi/mem_approx_scale. by have [m0_cmj _] := cmP j; apply/m0sym/m0_cmj/mem_approx_scale. exists (grid_map abP cmP ab_cmP); first exact: planar_bridgeless_grid_map. case/grid_map_coloring=> k0 ab_k0'. pose k z t := exists2 i, m0 (mr i) z & exists2 j, m0 (mr j) t & k0 i = k0 j. have mr_inj z t i j: m0 z t -> m0 (mr i) z -> m0 (mr j) t -> i = j. move=> m0zt m0iz m0jt; have [_] := mrP i; apply. exact/(m0tr (m0tr m0iz m0zt))/m0sym. exists k; last first. have p0: point by split; apply: Real.zero. exists (fun c => oapp mr p0 [pick i | k0 i == c :> nat]) => z [i m0iz _]. exists (k0 i); first exact/ltP/ltn_ord. have [j /eqP/val_inj-k0ij | /(_ i)/eqP] //= := pickP. by exists j; [have [] := mrP j | exists i]. have m0cover z t: m0 z t -> cover m0 z by move=> m0zt; apply/(m0tr m0zt)/m0sym. split=> [|z [i /m0sym/m0cover] // | z t m0zt | z t adj_zt [i m0iz [j m0jt]]]. - split=> z t [i m0iz [j m0jt k_ij]]; first by exists j => //; exists i. move=> t1 [i1 m0i1t [j1 m0jt1 k_j1]]; exists i => //; exists j1 => //. by rewrite k_ij (mr_inj t t j i1) //; apply: m0cover (m0sym m0jt). - by have /m0cover/mr_m0[i m0iz] := m0zt; do 2!exists i => //; apply: m0tr m0zt. without loss ltij: z t i j m0iz m0jt adj_zt / i < j. move=> IHij k0ij; have [m0'tz [u [corner'u [m0z_u m0t_u]]]] := adj_zt. have adj_tz: adjacent m0 t z by split=> [/m0sym|]; last exists u. have: i != j by case: eqP m0jt => // <- /(m0tr (m0sym m0iz)). by rewrite neq_ltn => /orP[/(IHij z t) | /(IHij t z)] []. have [m0'zt [u [corner'u [m0zu m0tu]]]] := adj_zt. apply/eqP/(ab_k0' (AdjIndex ltij))/ab_m0; split=> //; split=> [/= m0ij|]. by have [] := m0'zt; apply/(m0tr _ (m0tr m0ij m0jt))/m0sym. by do [exists u; do 2!split=> //]; [apply: m0tr_cl m0zu | apply: m0tr_cl m0tu]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph bigop ssralg ssrnum ssrint) mathcomp(div intdiv) fourcolor(hypermap geometry coloring grid matte gridmap) fourcolor(real realplane realprop approx)