proposition: Lemma in_refine_mdisk md p : (p \in refine_mdisk md) = (halfg p \in md).
proof: Proof. apply/flatten_mapP/idP=> [[x] | ] md_x; first by rewrite in_pmring => /eqP->. by exists (halfg p); last rewrite in_pmring inE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)