proposition: Lemma cubic_ecpN : quasicubic (rev (cpring ecpN)).
proof: Proof. pose qXe := [:: edge ecpN; icpN (face (edge x0)); icpN x0]. have cubic_qXe: cubicb (mem qXe). have cycNqXe: fcycle node qXe. by rewrite /= !eqxx -(inj_eq nodeI) edgeK -(eq_sym x0) (negPf x0gt1) eqxx. apply/subsetP=> u qXe_u; rewrite inE (order_cycle cycNqXe) //= andbT. by rewrite inE (inj_eq icpN_inj) (canF_eq (canF_sym nodeK)). apply/cubicP=> u; rewrite inE /= mem_rev -(mem_rot 1) rot1_cpring_ecpN. case qXe_u: (u \in qXe); first by clear 1; apply: (cubicP cubic_qXe). case: u qXe_u => [||x] //=. rewrite !inE (mem_map icpN_inj) !(inj_eq icpN_inj) !orFb. move/norP=> [fex0'x x0'x] p'x; rewrite (negPf x0'x). have{p'x} x0N'x: x \notin rev (cpring x0). case x0gt2: (long_cpring x0). move: p'x; rewrite (head_long_cpring x0gt2) rot1_cons /= drop0 mem_rcons. by rewrite mem_rev /= !inE !negb_or x0'x fex0'x. rewrite {p'x} mem_rev mem_cpring fconnect_orbit /orbit. have:= x0gt2; rewrite size_long_cpring size_cpring -orderSpred /= inE. rewrite (negPf x0'x); case: _.-1 => [|[|n]] //= _; rewrite inE. by move/eqP: x0gt2 => <-. have [n3x x'nx] := cubicP cubicG _ x0N'x; rewrite mem_rev mem_cpring in x0N'x. case: ifP => [/eqP nnx | x0'nnx]. by rewrite -nnx -2!cnode1 connect0 in x0N'x. split=> //=; rewrite n3x (negPf x0'x) (canF_eq nodeK) (negPf fex0'x). by rewrite /= x0'nnx n3x (canF_eq nodeK) (negPf fex0'x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)