proposition: Lemma refine_mring_cycle : cycle mrlink (refine_mring (mring m)).
proof: Proof. case: (mring m) (mring_cycle m) => // [d0 mr0]; rewrite !(cycle_path d0). rewrite [last _ _]/=; set d := last d0 mr0; set mr := d0 :: mr0. have ->: last d0 (refine_mring mr) = gface d *+ 2 + oddg d. by rewrite [mr]lastI /refine_mring -cats1 map_cat flatten_cat last_cat. elim: {d0 mr0}mr d => //= d2 _ IHmr d1 /andP[/eqP-Ed12 /IHmr{IHmr}->]. rewrite -!subr_eq /end1g !halfg_eq ?oddg_eq ?eqxx // andbC -addrA eqxx /=. by rewrite -[gface d1]end0g_eq oddg_face subrK end0g_face Ed12 end0g_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)