proposition: Theorem not_embed_reducible : False.
proof: Proof. have [et etGc etGr] := embed_contract. have{et etGc etGr}:= C_reducible_coclosure Cred_cc etGc embed_closure etGr. case=> et [kc [kcE kcF] Detc] [kr col_kr Detr]. apply: minimal_counter_example_is_noncolorable (cexGm) _. have [_] := colorable_patch ppGm; apply; exists (rev et); last first. by rewrite revK Detr -trace_rot -!map_rot rotrK; exists kr. exists (kc \o embd). split=> u. rewrite /= /embd_edge; case: ifP => _; first exact: kcE. by rewrite -(eqcP (kcF _)) nodeK; apply: kcE. by apply/eqP/(fconnect_invariant kcF); rewrite cface_embd -cface1. rewrite map_comp map_embd_ring Detc map_rev trace_rev rev_rot revK. suffices Drc: rc = map face (rot 1 erc). rewrite [in LHS]Drc -map_comp map_rot trace_rot rotK. by congr (trace _); apply: eq_map => x; apply/eqP/kcF. case: rc UNrc => // x p /andP[/=xNpx _]; rewrite rot1_cons. by elim: p {1 3}x xNpx => /= [|y p IHp] z /andP[/eqP/(canRL nodeK)-> // /IHp->]. 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)