On Perfect Matchings for some Bipartite Graphs

Inspired by some recent revisitations of the Cantor-Bernstein theorem, in particular its formalizations in ZF carried out via the proof assistant AProS by W. Sieg and P. Walsh, we are carrying out the proof of a related graph-theoretical proposition. Our development is assisted by the proof checker ÆtnaNova, and our proof pattern is drawn from Halmos’s classic ‘Naive set theory’. This case-study illustrates the flexibility of a proof environment rooted in Set Theory, which can be bent with equal ease toward declarative and procedural styles of proof.