proposition: Lemma in_refine_mring (mr : seq gpoint) d : reflect (exists2 d0, d0 \in mr /\ oddg d = oddg d0 & halfg d = d0 \/ halfg d = gface d0) (d \in refine_mring mr).
proof: Proof. apply: (iffP flatten_mapP) => [[d0 mr_d0 /mapP[p]] | [d0 [mr_d0 Dd] /pred2P]]. by rewrite !inE => /pred2P-Dp ->; rewrite !oddg_eq ?halfg_eq //; exists d0. by exists d0 => //; apply/mapP; exists (halfg d); rewrite ?inE // -Dd halfgK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)