Proof of `Trees are outerplanar`
conditional — 1 open assumptionproofs/Lax68Proofs/ForestMinors.lean · lax-68
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
A tree is acyclic, and so are all its minors. The triangle in and the four-cycle in therefore exclude both as minors. Apply the excluded-minor characterization of outerplanarity, which remains open in this submission.