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.
Exact expanded PA statement
forall n m k. n <= m -> m <= k -> n <= kStructural 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
Proof neighborhood
Direct dependencies
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_boundedFormal 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.
Read the argument
Proof checkpoints
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.
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–7
03Construct an explicit witnessL8–8
Supply the displayed value, then prove that it has the required property.
- 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.
- L9
simp [add_assoc, h_nm_witness, h_mk_witness]