proposition: Lemma in_extension xm : matte_extension xm -> {subset m <= xm}.
proof: Proof. elim: xm / => [|d xm0 xm _ IHxm _ Dxm] p m_p //. by rewrite Dxm mem_behead /= ?IHxm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)