proposition: Lemma refine_matte_coarse r : coarse_in r refine_matte.
proof: Proof. by move=> p q _ Dq; rewrite /= !in_refine_matte Dq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)