PA000R

le_trans

Stable checked-use theorem · independently closed

Order witnesses compose by addition, so the defined order is transitive.

Exact expanded PA statement

forall n m k. n <= m -> m <= k -> n <= k

Structural proof guide

Generated structural guide

Order witnesses compose by addition, so the defined order is transitive.

Use the direct prerequisites add_assoc as previously established PA formulas.

The proof proceeds by case analysis (2), certified simplification (1).

Referenced ingredients

PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA0009 add_assoc

Direct dependents

PA001R beta_moduli_coprime_of_lt_bounded_common_multiple PA001U beta_exclusive_accumulated_product_step PA002I bounded_beta_exclusive_recode_invariant PA002Q new_value_lt_scaled_base PA002T beta_value_lt_scaled_base PA006L lt_of_lt_of_le PA007C gauss_signed_half_magnitude_injective PA0097 finite_short_cover_impossible PA009Q pair_index_left_below_double PA009R pair_index_right_below_double PA00DR odd_half_division_quotient_bounded

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 n
  2. 0002intro m
  3. 0003intro k
  4. 0004intro h_nm
  5. 0005intro h_mk
  6. 0006cases h_nm
  7. 0007cases h_mk
  8. 0008exists x1 + x
  9. 0009simp [add_assoc, h_nm_witness, h_mk_witness]