proposition: Lemma ecpA_merge : cface (node ecpA) (node x0).
proof: Proof. rewrite edgeK /=; case ex0Fnx0: (cface (edge x0) (node x0)). by rewrite /ecpA_face ex0Fnx0 -cface1. have: cface (node x0) (edge (node (node x0))) by rewrite cface1r nodeK. case/connectP=> _ /shortenP[p nx0Fp Up _] Lp. have:= nx0Fp; rewrite -(map_path baseF_ecpA) ?map_id => [{}nx0Fp|]. rewrite (@cfaceC ecpA) (connect_trans (path_connect nx0Fp (mem_last _ _))) //. apply: connect1; rewrite -Lp /= /ecpA_face ex0Fnx0 nodeK eqxx. by rewrite (canF_eq (canF_sym faceK)); case: ifP. move: Up; rewrite lastI -Lp rcons_uniq => /andP[p'ennx0 _]. rewrite has_predU !has_pred1 negb_or p'ennx0 andbT. by apply: contraFN ex0Fnx0 => /mem_belast/(path_connect nx0Fp); rewrite cfaceC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)