BT00AA

finite_lt_succ_eq_or_lt

Stable · empty-context checked

A value below a successor is the predecessor or lies below it.

Exact expanded PA statement

forall n x. (exists h. h + S x = S n) -> x = n \/ exists h. h + S x = n

Structural proof guide

A value below a successor is the predecessor or lies below it.

Direct prerequisites: le_of_succ_le_succ, le_eq_or_lt. The authored body proceeds by intermediate claims (1).

Proof neighborhood

Direct dependencies

BT0017 le_of_succ_le_succ BT001C le_eq_or_lt

Direct dependents

BT00S0 prime_power_quotient_prefix_exists BT00SE eisenstein_initial_segment_prefix_extend BT00T2 beta_pascal_zero_row_extend BT00T4 beta_pascal_row_step_extend BT00T6 beta_pascal_table_prefix_extend BT00U7 primorial_factor_prefix_extend BT00UR primorial_interval_factor_prefix_extend BT00XW double_quotient_carry_prefix_extend BT00YP prime_contribution_prefix_extend BT010K prime_contribution_interval_prefix_extend

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 x
  3. 0003intro hlt
  4. 0004have hle : exists h. h + x = n
  5. 0005specialize le_of_succ_le_succ x
  6. 0006specialize le_of_succ_le_succ n
  7. 0007apply le_of_succ_le_succ
  8. 0008exact hlt
  9. 0009specialize le_eq_or_lt x
  10. 0010specialize le_eq_or_lt n
  11. 0011apply le_eq_or_lt
  12. 0012exact hle