proposition: Lemma iff_exists (T : Type) (P Q: T -> Prop) : (forall x, P x <-> Q x) -> (exists x : T, P x) <-> (exists x : T, Q x).
proof: Proof. firstorder. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)