BT0016

succ_le_succ

Stable · empty-context checked

Successor preserves the witness-defined order.

Exact expanded PA statement

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

Structural proof guide

Successor preserves the witness-defined order.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

BT0057 beta_value_lt_scaled_base BT0058 new_value_lt_scaled_base BT005E beta_prefix_product_trace_exists BT005K beta_product_succ_append BT0089 beta_prefix_sum_trace_exists BT00QF prime_power_exponent_le BT00TC choose_functional BT00TE choose_zero BT00TI choose_succ_succ_of_lt BT00TJ choose_succ_succ

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. 0005exists x
  6. 0006rewrite PA4
  7. 0007congr
  8. 0008exact h_witness