proposition: Lemma compactness_extension : colorable_with nc m0.
proof: Proof. by move: limit_coloring_coloring size_limit_coloring; exists limit_coloring. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)