proposition: Lemma check_reducible_valid : check_reducible -> cfreducible.
proof: Proof. rewrite /check_reducible /cfreducible; have:= contract_ctreeP cf. move: (cfcontract cf) (contract_ctree cf) => cc [] // cct [cc_ok cc_col] cc'K. split=> // et tr_et; have [k _ Det] := tr_et. have Eet: size (behead et) = (cprsize (cfprog cf)).-1. by rewrite size_behead Det size_trace size_map /cfring revK -size_ring_cpmap. have{cc'K cc_col tr_et} := ctree_mem_disjoint cc'K (cc_col et tr_et). move/(Kempe_treeP Eet){Eet}; rewrite -/(cfmap cf). have {k Det} <-: rot 1 et = ctrace (behead et). have: sumt et == Color0 by apply/eqP; rewrite Det; apply: sumt_trace. case: et Det => [|e et' _] /=. by rewrite revK head_cpring /= [ctrace _]headI. by rewrite rot1_cons /ctrace addc_eq0 => /eqP->. move=> IHet P closedP Pet; pose P1 (et1 : colseq) := P (rotr 1 et1). have{closedP} closedP1: Kempe_closed P1. move=> et1 /closedP[P1et1g [w et1Mw wPet1]]. split=> [h|]; first by rewrite /P1 -map_rotr; apply: P1et1g. exists (gram_rot w)=> [|et2]; first by rewrite -(rotrK 1 et1) match_gram_rot. by rewrite -{1}(rotrK 1 et2) match_gram_rot; apply: wPet1. rewrite -(rotK 1 et) in Pet. have{et IHet closedP1 Pet} [et [k col_k Det] P1et] := IHet _ closedP1 Pet. exists (rotr 1 et) => //; exists k => //. by rewrite revK Det map_rot trace_rot rotK. 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)