proposition: Fact ext2_P : {ir | rot ir.1 (mring m) = [:: gedge (gface d), gedge d & ir.2]}.
proof: Proof. have [i [|d1 r] Dr] := rot_to mr_efd. have /idPn[] := mring_cycle m; rewrite -(rot_cycle i) Dr /= /mrlink. by rewrite (inj_eq (addrI _)) neq_ccw. exists (i, r); rewrite Dr; congr [:: _, _ & _]. move: (mring_cycle m) mr_ed (mring_simple m). rewrite -(rot_cycle i) -(mem_rot i) -(rot_uniq i) -map_rot Dr. case/andP=> /eqP-Dd1 _; rewrite end1g_edge end0g_face -end0g_edge in Dd1. rewrite -(mem_rot 1) -(rot_uniq 1) -map_rot rot1_cons /= inE. by case/predU1P=> // r_ed; rewrite -Dd1 map_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)