PA000R · theorem

le_trans

Stable checked-use theorem · independently closed

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ n. ∀ m. ∀ k. Le(n,m) → Le(m,k) → Le(n,k)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0001 Le

3 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall n m k. n <= m -> m <= k -> n <= k

Proof neighborhood

Direct theorem prerequisites

PA0009 add_assoc

Direct theorem 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

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

9 script commands · 4 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro m
  3. L3
    intro k
  4. L4
    intro h_nm
  5. L5
    intro h_mk
02Separate the logical casesL6–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L6
    cases h_nm
  2. L7
    cases h_mk
03Construct an explicit witnessL8–8

Supply the displayed value, then prove that it has the required property.

  1. L8
    exists x1 + x
04Calculate and transport equalitiesL9–9

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L9
    simp [add_assoc, h_nm_witness, h_mk_witness]

Library-wide reading audit

Original defined command ledger · 9 lines
  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]