proposition: Lemma nontrivial_ring_proper : proper_ring r.
proof: Proof. case Dr: {1 3}r (andP nt_r) => [|x r1] [ntFr ntFCr]. by rewrite [fcard _ _]eq_card0 // in ntFr => y; apply: andbF. case: r1 {ntFr} => [|ex [|z r2]] // in Dr *. by have:= cycRr; rewrite Dr /= [rlink _ _]cfaceC bridgeless_cface. apply: contraTneq ntFCr => Dex; rewrite [fcard _ _]eq_card0 // => y. suffices dNy: y \in diskN r by rewrite !inE dNy !andbF. have{y} [p xCp ->] := connected_clink x y ccG. have rx: x \in r by rewrite Dr mem_head. elim/last_ind: p xCp => [|p y IHp]; first by rewrite /= diskN_E !inE rx. rewrite last_rcons rcons_path (fclosed1 (diskN_node r)) => /andP[/IHp dNp]. case/clinkP=> [<- // | /(canRL faceK) enx]; rewrite diskN_E orbC. rewrite (fclosed1 (diskE_edge geoG scycRr)) inE /= -{2}enx dNp andbT. by rewrite -(mem_rot 1) Dr !inE -Dex (can_eq ee) (canF_eq ee) orNb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry patch sew snip color chromogram) fourcolor(coloring kempe)