proposition: Lemma embed_contract : exists2 et, cc_ring_trace cc rrc et & embed_cotrace et.
proof: Proof. have [[rc'cc _ _ _] _] := Cred_cc; rewrite disjoint_has has_sym in rc'cc. have [k [kE kF]] := contract_coloring cexGm embed_valid_contract. pose k1 := k \o h1; exists (trace (map k1 rrc)). exists k1; split. have k1Ebc x: x \in bc -> invariant edge k1 x = (x \in insertE cc). move=> bc_x; rewrite /k1 /= embedE [_ == _]kE mapEh1. apply/mapP/idP=> [[y c_y /embed_inj-> //]|]; last by exists x. exact: (hasPn rc'cc). move=> x; have /orP[|bc_ex] := edge_perimeter x; first exact: k1Ebc. rewrite mem_insertE // (eq_has (cedge1 x)) -mem_insertE // -k1Ebc //= e2c. by rewrite eq_sym. move=> x; rewrite /k1 /=. by rewrite -(fconnect_invariant kF (cface_h1 (fconnect1 face x))) eqxx. exists (k \o embr). split=> w /=. rewrite [_ == _]kE mapEh1; apply: contraNF (valP w) => /mapP[x cc_x /= ->]. have xdP: x \in codom embd by rewrite codom_embd; apply: (hasPn rc'cc). apply/imageP; exists (iinv xdP); rewrite /embdd ?f_iinv // inE /=. rewrite -(mem_map embd_inj) map_embd_ring f_iinv -[x]e2c (mem_map edgeI). by apply: (hasPn rc'cc); apply: ccE. by apply/eqP/(fconnect_invariant kF); rewrite -(patch_face_r ppGm) -cface1. rewrite !map_rotr 2!map_comp map_embr_ring (map_comp h1 embd) map_embd_ring. rewrite !map_rev -rev_rot; congr (trace (rev _)). case: rc cycNrc => //= x p; rewrite rot1_cons. elim: p {1 3}x => [|_ p IHp] y /= /andP[/eqP <- nyNp]. congr [:: _]; apply/(fconnect_invariant kF)/cface_h1. by rewrite cface1r nodeK. congr (_ :: _); last exact: IHp. by apply/(fconnect_invariant kF)/cface_h1; rewrite cface1r nodeK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring patch) fourcolor(snip revsnip kempe birkhoff contract)