proposition: Lemma nontrivial_cycle2 (x y : G) (r := [:: x; y]) : scycle rlink r -> edge x != y -> nontrivial_ring 0 r.
proof: Proof. move=> Ur y'ex; apply/nontrivial0P; split. exists (node x); rewrite !inE -(fclosed1 (diskN_node r)). rewrite diskN_E mem_head unfold_in /= -{2}[x]nodeK -cface1r. rewrite bridgeless_cface //= orbF andbT; apply: contraL Ur => nxFy /=. rewrite /rlink -(same_connect_r cfaceC nxFy) -[node x]nodeK -cface1r. by rewrite cface1 -(canRL nodeK (nnn x)) bridgeless_cface. pose nex := node (edge x); have rF'nex: nex \notin fband r. rewrite unfold_in /= orbF -{1}[nex]nodeK -cface1 (canRL nodeK (nnn _)) ee. rewrite cfaceC cface1 bridgeless_cface //; apply: contraL Ur => /= nexFy. rewrite {1}/rlink -(same_connect_r cfaceC nexFy) -[edge x]nodeK -cface1. by rewrite cfaceC bridgeless_cface. exists nex; rewrite !inE rF'nex -(fclosed1 (diskN_node r)) diskN_E inE /=. by rewrite -(fclosed1 (diskE_edge planarG Ur)) !inE e'id eqxx (negPf y'ex). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan geometry color chromogram) fourcolor(coloring patch snip sew revsnip kempe) fourcolor(ctree initctree gtree initgtree ctreerestrict) fourcolor(gtreerestrict cfmap cfcolor kempetree)