proposition: Lemma cpring_ecpA : cpring ecpA = (if long_cpring x0 then behead (behead (cpring x0)) else cpring x0).
proof: Proof. case x0gt2: (long_cpring x0). apply cpring_def; first by rewrite (head_long_cpring x0gt2) edgeK. apply/andP; split; last first. rewrite rev_uniq; have:= cpring_uniq x0; rewrite (head_long_cpring x0gt2). by case/and3P. move: (cycle_rev_cpring x0); rewrite (head_long_cpring x0gt2) /= !rev_cons. do 4![rewrite -rot1_cons rot_cycle -?rcons_cons] => /= /and3P[_ _]. have nAfex0: ecpA_node (face (edge x0)) = node (node x0). by rewrite /ecpA_node -(inj_eq nodeI) edgeK eqxx; case: eqP. case Dp: (rev (drop 3 (cpring x0))) => [|x p]; rewrite /= nAfex0 //. rewrite -(map_path baseN_ecpA) ?map_id // belast_rcons has_predU !has_pred1. move: (cpring_uniq x0); rewrite (head_long_cpring x0gt2) -Dp !mem_rev /= !inE. by rewrite !negb_or => /and4P[/and3P[_ _ ->]]. apply cpring_def; first by move/eqP: x0gt2; rewrite head_cpring edgeK. rewrite /ucycle rev_uniq /= cpring_uniq andbT. move: x0gt2 (cycle_rev_cpring x0) (cpring_uniq x0). rewrite size_long_cpring head_cpring /= /ecpA_node. case: (behead _) => [|x[]] //= _; rewrite !andbT !eqxx (inj_eq nodeI) eq_sym //. by case/andP=> /eqP-> _; rewrite inE eqxx andbT eq_sym => /negPf->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)