proposition: Lemma ext1_mring_simple : uniq (map end0g ext1_mring).
proof: Proof. rewrite /ext1_mring; case: (rot_to _) => i r Dr. case: (mring_equad m'f4d, mring_simple m); rewrite -(rot_uniq i) -(mem_rot i). move: (mring_equad m'f3d); rewrite -[LHS](mem_rot i) -map_rot {i}Dr. rewrite !map_cons !inE !end0g_edge -!end0g_face. move: {r}(map _ r) (gface d) => r d1 /=; rewrite !inE ![_ == end0g d1]eq_sym. move=> /norP[/negPf-> /negPf->] /norP[/negPf-> /negPf->] /andP[-> ->] /=. by rewrite eq_sym end0g_face (inj_eq (addrI _)) neq_ccw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)