proposition: Lemma cpring_ecpU : cpring ecpU = [:: node ecpU, ecpU : ecpU & map icpU (cpring x0)].
proof: Proof. apply: cpring_def => //; apply/andP; split. move: (cpring_uniq x0) (cycle_rev_cpring x0); rewrite head_cpring /=. rewrite !rev_cons -map_rev -mem_rev -rev_uniq; move: (rev _) => p /andP[Up _]. do 4 rewrite -rot1_cons rot_cycle -?rcons_cons; rewrite /= !eqxx -map_rcons. case: p Up => [|x p] Up //=; rewrite (map_path baseN_ecpU) //. by rewrite belast_rcons -has_map has_pred1 (mem_map icpU_inj). rewrite rev_uniq /= !inE (map_inj_uniq icpU_inj) cpring_uniq andbT. by do 2?case: mapP => [[] | _] //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)