proposition: Lemma red588to633 : reducible_in_range 588 633 the_configs.
proof: Proof. have red633: reducible_in_range 633 633 the_configs. by apply check_reducible_in_range; left. CatReducible red588to610 red610to617 red617to622 red622to633 red633. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq) fourcolor(cfmap cfreducible configurations) fourcolor(job589to610 job611to617 job618to622 job623to633)