proposition: Lemma ext1_mring_cycle : cycle mrlink ext1_mring.
proof: Proof. rewrite /ext1_mring; case: (rot_to _) => i r Dr. have:= mring_cycle m; rewrite -(rot_cycle i) {i}Dr !(cycle_path d) /=. rewrite /mrlink !end0g_face !eqxx /= end0g_edge. by case: r => [|d1 r]; rewrite /= end1g_edge -!end0g_face gface4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)