proposition: Lemma refine_mring_def : refine_mring (mring m) =i gborder (refine_mdisk m).
proof: Proof. move: (mdisk m) (in_mring m) => md Dmr d. rewrite inE !in_refine_mdisk halfg_edge halfg_add; set p := halfg d. apply/in_refine_mring/andP=> [[d1 [mr_d1 Dd] Dp] | [md_p md'ep]]. rewrite Dmr !inE halfg_edge -/p in mr_d1 Dp; have [md_d1] := andP mr_d1. by case: Dp => ->; rewrite ?halfg_face ?oddg_face -Dd; case: oddgP. have Dd: pred2 (oddg d) (ccw (oddg d)) (oddg p). by have/(memPn md'ep):= md_p; rewrite addrC -subr_eq subrr; do 2!case: oddgP. exists (halfg p *+ 2 + oddg d). rewrite Dmr !inE halfg_edge halfg_eq ?oddg_eq ?md_p //. by case: (oddgP d) (oddgP p) Dd md'ep => -[] //. rewrite gface_def oddg_eq ?halfg_eq //. by case/pred2P: Dd => <-; [left | right]; rewrite halfgK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)