proposition: Lemma check_reducible_in_range j1 j2 (cfs : seq config) : (forall i, let n := j2 - j1 in n <= i \/ check_reducible (nth cf000 (take n (drop j1 cfs)) i)) -> reducible_in_range j1 j2 cfs.
proof: Proof. move=> red_j12 i j1_le_i i_lt_j2; set n := j2 - j1; set i' := i - j1. have le_j12: j1 <= j2 by apply ltnW; apply: leq_trans i_lt_j2. have i'_lt_n: i' < n by rewrite -subSn // leq_subLR subnKC. case: {red_j12}(red_j12 i'); rewrite -/n; first by rewrite leqNgt i'_lt_n. by rewrite nth_take // nth_drop subnKC //; apply: check_reducible_valid. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring kempe) fourcolor(cfmap cfcolor cfcontract ctree kempetree)