proposition: Lemma the_reducibility : reducibility.
proof: Proof. rewrite /reducibility; apply cat_reducible_range with 322. CatReducible red000to214 red214to234 red234to282 red282to302 red302to322. CatReducible red322to485 red485to506 red506to541 red541to588 red588to633. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq) fourcolor(cfmap cfreducible configurations present) fourcolor(task001to214 task215to234 task235to282) fourcolor(task283to302 task303to322 task323to485) fourcolor(task486to506 task507to541 task542to588) fourcolor(task589to633)