proposition: Lemma exists_map_repr : exists n, exists2 mr : map_repr n, mr_proper mr & subregion (cover m0) (mr_cover mr).
proof: Proof. have [_ [k [mr0 sm0r0]]] := fin_m0; pose mr0k : map_repr k := mr0. suffices{sm0r0} [n [mr mrP sr0mr]]: exists n, exists2 mr : map_repr n, mr_proper mr & subregion (mr_cover mr0k) (mr_cover mr). - by exists n, mr => // z /sm0r0[i /ltP-lti ?]; apply/sr0mr; exists (sub i lti). elim: k @mr0k => [|k [n [mr mrP]] sr0mr]; last pose t := mr0 k. by exists 0, (fun=> mr0 0) => [|z []] []. have [mr_t | mr't] := Rclassic (cover m0 t -> mr_cover mr t). exists n, mr => // z [j]; have{j} [j -> m0jz | -> m0tz] := unliftP ord_max j. by rewrite lift_max in m0jz; apply/sr0mr; exists j. have [i m0it]: mr_cover mr t by apply/mr_t/(m0tr m0tz)/m0sym. by exists i; apply/(m0tr m0it). exists n.+1, [fun i => oapp mr t (unlift ord0 i)] => [i1 | z [j]] /=. case: unliftP => [i|] -> {i1}/=. have [m0i Imr_i] := mrP i; split=> {m0i}// j1. by case: unliftP => [j -> /Imr_i|] -> //= m0it; case: mr't; exists i. split=> [|j1]; first by case: (Rclassic (cover m0 t)) mr't => // m0't []. by case: unliftP => //= j _ /m0sym-m0jt; case: mr't; exists j. have{j} [j -> m0jz | -> /= m0tz] := unliftP ord_max j; last first. by exists ord0; rewrite /= unlift_none. suffices [i m0iz]: mr_cover mr z by exists (lift ord0 i); rewrite /= liftK. by rewrite lift_max in m0jz; apply/sr0mr; exists j. 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)