BT000W

zero_le

Stable · empty-context checked

Zero is below every natural number.

Exact expanded PA statement

forall n. 0 <= n

Structural proof guide

Zero is below every natural number.

Direct prerequisites: none. The authored body proceeds by equality transport (1).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT005E beta_prefix_product_trace_exists BT005K beta_product_succ_append BT0089 beta_prefix_sum_trace_exists BT00Q6 bounded_power_valuation_exists BT00QF prime_power_exponent_le BT00TE choose_zero BT00XG division_double_quotient_bit

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro n
  2. 0002exists n
  3. 0003rewrite PA3
  4. 0004refl