PA003U

ne_zero_of_one_le

Stable checked-use theorem · independently closed

A natural at least one is nonzero.

Exact expanded PA statement

forall n. 1 <= n -> ~(n = 0)

Structural proof guide

Generated structural guide

A natural at least one is nonzero.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by case analysis (1), equality transport (2).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA007D beta_magnitude_predecessor_recode_exists PA007S beta_magnitude_predecessor_recode_bounded PA007T beta_magnitude_predecessor_recode_reflect PA00AG prime_bounded_square_one_cases

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. 0003intro hn
  4. 0004cases h
  5. 0005rewrite hn at h_witness
  6. 0006apply PA1
  7. 0007rewrite PA4 at h_witness
  8. 0008exact h_witness