proposition: Lemma refine_mring_simple : uniq (map end0g (refine_mring (mring m))).
proof: Proof. have /hasPn := @mring_edge m; move: (mring m) (mring_simple m). elim=> //= d r IHr /andP[r'd Ur] /norP[_]; rewrite has_predU => /norP[r'E /IHr]. move=> -> {Ur}//; rewrite !/(end0g _) !halfg_eq ?oddg_eq // inE -addrA subrK. rewrite (inj_eq (addrI _)) eq_sym neq_ccw /= andbC. rewrite !(contra _ r'd) /end0g // => /mapP[d1 /in_refine_mring[d0 [r_d0 ->]]]. case=> -> Dd; first by rewrite -[_ + _]halfg_add_odd Dd halfg_add_odd map_f. have /eqP/idPn[]:= congr1 oddg Dd; rewrite oddg_add oddg_double. by rewrite oddg_add oddg_face; case: (oddgP d0). case=> -> Dd; last rewrite -addrA subrK in Dd. have:= congr1 oddg Dd; rewrite [RHS]oddg_add oddg_double. by rewrite oddg_add; case: (oddgP d). suff Dd0: oddg d0 = oddg d by move: Dd; rewrite Dd0 => /addIr->; apply: map_f. have:= congr1 oddg Dd; rewrite oddg_add [RHS]oddg_add. have{r'E r_d0}: gedge d0 != d := hasPn r'E d0 r_d0. by rewrite /gedge 2!addrA -Dd -!addrA -subr_eq0 addrC addKr; do 2!case: oddgP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)