BT001C

le_eq_or_lt

Stable · empty-context checked

A witnessed inequality is either equality or a witnessed strict inequality.

Exact expanded PA statement

forall a b. (exists k. k + a = b) -> a = b \/ exists k. k + S a = b

Structural proof guide

A witnessed inequality is either equality or a witnessed strict inequality.

Direct prerequisites: zero_or_succ, zero_add, add_succ_left. The authored body proceeds by case analysis (3), equality transport (3).

Proof neighborhood

Direct dependencies

BT000Q zero_or_succ BT0000 zero_add BT0001 add_succ_left

Direct dependents

BT002U gcd_exists_up_to BT0034 gcd_balanced_bezout_exists_up_to BT003D factor_property_succ BT003J proper_factor_lt BT0059 beta_exclusive_accumulated_product_step BT005A beta_exclusive_recode_congruence_step BT005E beta_prefix_product_trace_exists BT005K beta_product_succ_append BT0069 beta_factor_divides_product BT007V beta_repeat_succ_extend BT0085 beta_range_succ_extend BT0089 beta_prefix_sum_trace_exists BT0097 lt_three_cases BT00AA finite_lt_succ_eq_or_lt BT00JD eisenstein_initial_segment_bit_count_functional BT00PS bounded_prime_interval_search BT00Q5 bounded_power_valuation_search BT00RA floor_sqrt_total BT00SG division_remainder_successor_cases BT00VV primorial_le_four_pow_bounded BT00VY no_bertrand_central_prime_divisor_le BT00W2 no_bertrand_central_prime_divisor_ranges BT00WW bertrand_hj_base_window_thirty_two_from_total BT00XG division_double_quotient_bit BT010D floor_sqrt_three_mul_le_double BT011A prime_le_twenty_two_cases BT0127 bertrand_strict

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004cases h
  5. 0005specialize zero_or_succ x
  6. 0006cases zero_or_succ
  7. 0007left
  8. 0008rewrite zero_or_succ_left at h_witness
  9. 0009specialize zero_add a
  10. 0010rewrite zero_add at h_witness
  11. 0011exact h_witness
  12. 0012cases zero_or_succ_right
  13. 0013right
  14. 0014exists x1
  15. 0015trans S x1 + a
  16. 0016trans S (x1 + a)
  17. 0017apply PA4
  18. 0018symm
  19. 0019apply add_succ_left
  20. 0020rewrite <- zero_or_succ_right_witness
  21. 0021exact h_witness