Exact expanded PA statement
forall n m. n <= m \/ m <= nStructural proof guide
Generated structural guide
Every pair of natural numbers is comparable in the defined order.
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by structural induction (2), case analysis (3), equality transport (2), certified simplification (2).
Referenced ingredients
none
Proof neighborhood
Direct dependencies
none
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
- 0001
induction n - 0002
intro m - 0003
left - 0004
exists m - 0005
simp - 0006
induction m - 0007
right - 0008
exists (S n) - 0009
simp - 0010
specialize IH m - 0011
cases IH - 0012
cases IH_left - 0013
left - 0014
exists x - 0015
rewrite PA4 - 0016
congr - 0017
exact IH_left_witness - 0018
cases IH_right - 0019
right - 0020
exists x - 0021
rewrite PA4 - 0022
congr - 0023
exact IH_right_witness