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