proposition: Lemma red485to506 : reducible_in_range 485 506 the_configs.
proof: Proof. CatReducible red485to489 red489to494 red494to498 red498to502 red502to506. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq) fourcolor(cfmap cfreducible configurations) fourcolor(job486to489 job490to494 job495to498) fourcolor(job499to502 job503to506)