To prove an existential statement, one uses the tactic exists, supplying it with a so-called witness.
Created [01 Feb 2024]
Structural induction over Peano numbers
Specifications
Enter search terms or a module, class or function name.