proposition: Lemma in_refine_matte p : (p \in refine_matte) = (halfg p \in m).
proof: Proof. exact: in_refine_mdisk. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)