proposition: Lemma scycle_planar_bridgeless_plain_quasicubic_connected_is_scycle : scycle_planar_bridgeless_plain_quasicubic_connected -> sfcycle node r.
proof: Proof. by do 3![case] => _ /andP[] *; apply/andP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)