proposition: Lemma cpring_ecpN : cpring ecpN = if long_cpring x0 then [:: icpN (node x0), ecpN : ecpN & map icpN (drop 3 (cpring x0))] else [:: ecpN : ecpN].
proof: Proof. case: ifP => [x0gt2 | x0le1]; last first. by apply cpring_def; rewrite /ucycle /= /frel /ecpN_node x0le1. apply cpring_def; [by rewrite /= x0gt2 | apply/andP; split]. move: (cpring_uniq x0) (cycle_rev_cpring x0). rewrite (head_long_cpring x0gt2) /= drop0; move: (drop 3 _) => p. rewrite !rev_cons -map_rev !inE -!(mem_rev p) -rev_uniq !negb_or. move: {p}(rev p) => p /and4P[/and3P[x0'nx0 _ p'nx0] /andP[_ p'x0] _ Up]. do 5!rewrite -rot1_cons rot_cycle -?rcons_cons. rewrite (cycle_path x0) (cycle_path (IcpX G)) /= last_map. case/and4P=> /eqP Lp _ _ nx0Np. rewrite (map_path baseN_ecpN) ?has_predU ?has_pred1 /ecpN_node ?x0gt2 /=. by rewrite -(inj_eq nodeI) Lp edgeK (negPf x0gt2) !eqxx. apply/orP; case => [/mem_belast|]; first by rewrite inE eq_sym=> /norP[]. have: uniq (node x0 :: p) by rewrite /= p'nx0. by rewrite -Lp nodeK lastI rcons_uniq => /andP[/negP]. have:= cpring_uniq x0; rewrite (head_long_cpring x0gt2) rev_uniq /= drop0. move: (drop 3 _) => p; rewrite !inE (map_inj_uniq icpN_inj) (mem_map icpN_inj). by rewrite orbA => /and4P[/norP[_ ->] _ _ ->]; case: mapP => [[]|]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)