PA001B

le_zero

Stable checked-use theorem · independently closed

Only zero is less than or equal to zero.

Exact expanded PA statement

forall n. n <= 0 -> n = 0

Structural proof guide

Generated structural guide

Only zero is less than or equal to zero.

Use the direct prerequisites add_eq_zero_right as previously established PA formulas.

The proof proceeds by case analysis (1).

Referenced ingredients

PA0004 add_eq_zero_right

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right

Direct dependents

PA001K gcd_balanced_bezout_exists_up_to PA0035 gcd_exists_up_to PA00DX eisenstein_initial_segment_bit_count_functional

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.

  1. 0001intro n
  2. 0002intro h
  3. 0003cases h
  4. 0004apply add_eq_zero_right
  5. 0005exact h_witness