BT000Y

le_zero

Stable · empty-context checked

Only zero is less than or equal to zero.

Exact expanded PA statement

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

Structural proof guide

Only zero is less than or equal to zero.

Direct prerequisites: add_eq_zero_right. The authored body proceeds by case analysis (1).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right

Direct dependents

BT002U gcd_exists_up_to BT0034 gcd_balanced_bezout_exists_up_to BT003E factor_search_up_to BT003K prime_divisor_exists_up_to BT0097 lt_three_cases BT00JD eisenstein_initial_segment_bit_count_functional BT00PS bounded_prime_interval_search BT00Q5 bounded_power_valuation_search BT00TM choose_positive BT00VV primorial_le_four_pow_bounded

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. 0002intro h
  3. 0003cases h
  4. 0004apply add_eq_zero_right
  5. 0005exact h_witness