proposition: Lemma refine_matte_ne : ~~ nilp (refine_mdisk m).
proof: Proof. by case: (mdisk m) (matte_ne m). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)