Add the Neumann-Lara and Tait conjectures on planar graphs and digraphs (directed graphs)

Title: The Neumann-Lara and Tait conjectures on planar graphs

### What is the conjecture

This issue collects two famous conjectures on planar graphs and digraphs (directed graphs).

1. **Neumann-Lara conjecture** (1985; independently Škrekovski). The dichromatic number of a digraph is the least number of colors needed to color its vertices so that each color class induces an acyclic subdigraph. The conjecture states that every planar digraph of digirth at least 3 (an oriented planar graph) has dichromatic number at most 2. It is known for digirth at least 4 (Li and Mohar), for graphs on at most 26 vertices (Knauer and Valicov), and it is equivalent, by a result of Steiner, to the 2-dicolorability of orientations of `K₅`-minor-free graphs.
2. **Tait's conjecture** (1884), which is false. It states that every 3-connected planar cubic graph has a Hamiltonian cycle. Tait proposed it as a route to the four color theorem, and Tutte (1946) gave a counterexample, the 46-vertex Tutte graph. The statement is recorded here as `answer(False)`.

References:
- V. Neumann-Lara, *The dichromatic number of a digraph*, Journal of Combinatorial Theory Series B 33 (1982), 265–270. The planar conjecture is attributed to Neumann-Lara (1985) and independently to Škrekovski.
- Z. Li and B. Mohar, [*Planar digraphs of digirth four are 2-colorable*](https://doi.org/10.1137/16M108080X), SIAM Journal on Discrete Mathematics 31(3) (2017), 2201–2205. Open-access version: [arXiv:1606.06114](https://arxiv.org/abs/1606.06114).
- R. Steiner, [*A note on graphs of dichromatic number 2*](https://dmtcs.episciences.org/7040), Discrete Mathematics & Theoretical Computer Science 21 (2019).
- P. G. Tait, *Listing's Topologie*, Philosophical Magazine (5th series) 17 (1884), 30–46.
- W. T. Tutte, *On Hamiltonian circuits*, Journal of the London Mathematical Society 21 (1946), 98–101.
- [Dichromatic number (Wikipedia)](https://en.wikipedia.org/wiki/Dichromatic_number)
- [Tait's conjecture (Wikipedia)](https://en.wikipedia.org/wiki/Tait%27s_conjecture)

### Prerequisites needed

Both conjectures need a planarity predicate, which Mathlib does not yet have. Planarity is defined combinatorially through Wagner's theorem (a finite graph is planar if and only if it has neither `K₅` nor `K₃,₃` as a minor), which in turn needs a graph-minor relation (`SimpleGraph.IsMinor`). The latter is currently proposed in the open PR #5196; the PR here adds the Wagner-planarity layer on top of it.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05 Combinatorics

### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start with open PR #5196, which proposes SimpleGraph.IsMinor, then trace how the Wagner-planarity layer should build on it. Formalize the Neumann-Lara and Tait statements described in the issue, including Tait's conjecture as false, and verify that both use the resulting planarity predicate.

Written by the indexing model from the issue text.