proposition: Lemma adjC : plain G -> symmetric adj.
proof: Proof. move=> plainG; apply: symmetric_from_pre => x y /adjP[z xFz zRy]. by apply/adjP; exists (edge z); rewrite /rlink cfaceC ?plain_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)