proposition: Lemma ext1_mring_def : ext1_mring =i gborder (ext_mdisk d).
proof: Proof. move=> p; rewrite /ext1_mring; case: (rot_to _) => i r Dr. have [m'ef1d m'ef2d m'ef3d _] := and4P m'Eloop; rewrite !inE !(eq_sym p). have [<- | p'f1d] := altP eqP. by rewrite halfg_face eqxx m'd /= eq_sym -halfg_face neq_halfg_edge. have [<- | p'f2d] := altP eqP. by rewrite !halfg_face eqxx m'd /= eq_sym -2!halfg_face neq_halfg_edge. have [<- | p'f3d] := altP eqP. by rewrite !halfg_face eqxx m'd /= eq_sym -3!halfg_face neq_halfg_edge. rewrite /= negb_or andbCA andb_orl -[rhs in _ || rhs]in_mring orbC andbC. have [mr_p | mr'p] /= := boolP (p \in mring m). have [/andP[r'ed _]]: uniq (gedge d :: r) /\ p \in gedge d :: r. by rewrite -Dr rot_uniq mem_rot (map_uniq (mring_simple m)). rewrite inE => /predU1P[->|r_p]; first by rewrite gedge2 eqxx (negPf r'ed). move: mr_p; rewrite in_mring => /andP[/contraTneq->//] /esym/same_halfg. by rewrite !inE !(inv_eq gedge2) -implyNb (memPn r'ed) //= => /or3P[]/eqP->. apply/negb_inj; have /norP[_ ->]: p \notin gedge d :: r by rewrite -Dr mem_rot. apply/esym/nandP; left; apply: contraL rm_ed => /andP[/eqP/esym/same_halfg]. rewrite !inE in_mring negb_and => /predU1P[-> -> //|/norP[]]. by rewrite !(eq_sym p) negb_or p'f2d. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)