proposition: Lemma ext2_mring_def : ext2_mring =i gborder (ext_mdisk d).
proof: Proof. rewrite /ext2_mring; case: ext2_P => -[i r] /= Dr p; rewrite !inE. have [m'ef2d m'ef3d _] := and3P m'Eloop. have [-> | f2d'p] /= := altP eqP. by rewrite andbC eq_sym -2!halfg_face eqxx neq_halfg_edge andbT. have [-> | f3d'p] /= := altP eqP. by rewrite andbC eq_sym -3!halfg_face eqxx neq_halfg_edge andbT. rewrite negb_or andbCA andb_orl -[rhs in _ || rhs]in_mring orbC andbC. have [mr_p | mr'p] /= := boolP (p \in mring m). apply/esym; apply/eqP/idP=> [|[/esym/same_halfg/(map_f gedge)Dp r_p]]. have:= mr_p; rewrite -(mem_rot i) Dr !inE orbA. by case/orP; [case/pred2P=> ->; left; rewrite gedge2 ?halfg_face | right]. have:= map_uniq (mring_simple m); rewrite -(rot_uniq i) Dr. rewrite (cat_uniq [:: _; _]) andbCA andbC => /andP[_] /hasPn/(_ p r_p). rewrite !inE orbC => p'efd; rewrite gedge2 !inE orbA (negPf p'efd) /= in Dp. by have:= mr_p; rewrite in_mring => /nandP[]; left; case/pred2P: Dp => ->. have:= mr'p; rewrite -(mem_rot i) Dr !inE orbA => /norP[_ /negPf->]. apply/esym/nandP; left; apply: contraL mr_efd => /andP[/eqP/esym/same_halfg]. rewrite !inE (negPf f2d'p) (negPf f3d'p) !orbF in_mring negb_and gedge2. by rewrite halfg_face m'd orbF => /pred2P[->|<-//]; have [->] := andP ext2d. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)