Graph Theory v0.9

The main changes in this release are:

• A proof of the main direction of Wagner's theorem using hypermaps and supporting libraries (requires coq-fourcolor):
  • hmap_ops.v: operations on hypermaps
  • hcycle.v : faces of two-connected grahs are bounded by cycles
  • embedding.v : combinatorial (plane) embeddings for simple graphs
  • K4plane.v : a plane embedding for K4
  • wagner.v : main direction of Wagner's theorem and structural four-color theorem
• A proof of the weak perfect graph theorem (WPGT)
  • partition.v : basic lemmas about partitions
  • coloring.v : definitions and lemmas about stable set number, clique number, and chromatic number.
  • wpgt.v : perfect graphs and two proofs of the WPGT (via Lovasz replication lemma and via matrix rank argument)
• the concept of k-connectivity and associated lemmas (connectivity.v).
• a substantial collection of lemmas on the arc predicate (new file: arc.v).
• lemmas about the operation of merging two vertices (new file: smerge.v)

This release is compatible with mathcomp-1.12 on coq-8.12and coq-8.13.