BT0019

lt_to_le

Stable · empty-context checked

A witnessed strict inequality entails the corresponding weak inequality.

Exact expanded PA statement

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

Structural proof guide

A witnessed strict inequality entails the corresponding weak inequality.

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

Proof neighborhood

Direct dependencies

BT0001 add_succ_left

Direct dependents

BT0059 beta_exclusive_accumulated_product_step BT005A beta_exclusive_recode_congruence_step BT00PR prime_strictly_above_decidable BT00R1 ceil_div_six_total BT00T6 beta_pascal_table_prefix_extend BT00TA beta_pascal_row_step_pointwise_functional BT00TB beta_pascal_table_row_pointwise_functional BT00TF beta_pascal_table_diagonal_boundary BT00TI choose_succ_succ_of_lt BT00X4 bertrand_floor_power_product_le_h_from_total BT00YI central_binom_prime_above_floor_sqrt_valuation_le_one BT00YL no_bertrand_central_nonzero_contribution_factor_ranges BT010V no_bertrand_small_contribution_choice_le_double

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 S x
  6. 0006trans x + S a
  7. 0007trans S (x + a)
  8. 0008apply add_succ_left
  9. 0009symm
  10. 0010apply PA4
  11. 0011exact h_witness