PA000W

le_eq_or_lt

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites zero_or_succ, zero_add, add_succ_left as previously established PA formulas.

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

Referenced ingredients

PA0008 zero_or_succ PA0001 zero_add PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA0008 zero_or_succ PA0001 zero_add PA000E add_succ_left

Direct dependents

PA001K gcd_balanced_bezout_exists_up_to PA001U beta_exclusive_accumulated_product_step PA002G beta_exclusive_recode_congruence_step PA002Y beta_range_succ_extend PA0035 gcd_exists_up_to PA003D finite_lt_succ_eq_or_lt PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA0044 beta_repeat_succ_extend PA005L quadratic_residue_search_up_to PA00B4 finite_bounded_nonendpoint_injective_coverage PA00BB pair_order_terminal_state_magnitude_range 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 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