proposition: Lemma kernel_off_ring : kernel \subset [predC p].
proof: Proof. by rewrite -disjoint_subset disjoint_sym -subset_disjoint ring_fband. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)