EC0004

euclidean_add_right_preserves_lt

Constructive strict natural order remains strict after adding the same right summand.

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable

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.

G101 was OPEN when this family was first admitted in Alpha v21. It is now CLOSED in Alpha v23: the actual anchored Euclidean history, terminal gcd, and exact bound steps≤2*BitLen(b)+1 are proved.

Exact theorem in conservative defined notation

∀ r. ∀ b. ∀ t. Lt(r,b) → Lt(r + t,b + t)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Lt(a,b) · 2

Actual proof prerequisites

add_le_add_right · checked external prerequisiteadd_succ_left · checked external prerequisite
Original expanded first-order statement 
forall r b t. (exists ff_lt_ec_add_strict. ff_lt_ec_add_strict + S r = b) -> (exists ff_lt_ec_add_shifted. ff_lt_ec_add_shifted + S (r + t) = (b + t))

Complete unchanged native tactic proof

All 16 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

16 script commands · 8 reading checkpoints · 1 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–4

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

  1. L1
    intro r
  2. L2
    intro b
  3. L3
    intro t
  4. L4
    intro hlt
02Use earlier factsL5–7

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L5
    specialize add_le_add_right (S r)
  2. L6
    specialize add_le_add_right b
  3. L7
    specialize add_le_add_right t
03Establish hshiftL8–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add le add right.

  1. L8
    have hshift : exists gap. gap + (S r + t) = b + t
  2. L9
    apply add_le_add_right
  3. L10
    exact hlt
04Separate the logical casesL11–11

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

  1. L11
    cases hshift
05Construct an explicit witnessL12–12

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

  1. L12
    exists x
06Use earlier factsL13–14

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L13
    specialize add_succ_left r
  2. L14
    specialize add_succ_left t
07Calculate and transport equalitiesL15–15

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

  1. L15
    rewrite add_succ_left at hshift_witness
08Use earlier factsL16–16

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L16
    exact hshift_witness

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro r
  2. 0002intro b
  3. 0003intro t
  4. 0004intro hlt
  5. 0005specialize add_le_add_right (S r)
  6. 0006specialize add_le_add_right b
  7. 0007specialize add_le_add_right t
  8. 0008have hshift : exists gap. gap + (S r + t) = b + t
  9. 0009apply add_le_add_right
  10. 0010exact hlt
  11. 0011cases hshift
  12. 0012exists x
  13. 0013specialize add_succ_left r
  14. 0014specialize add_succ_left t
  15. 0015rewrite add_succ_left at hshift_witness
  16. 0016exact hshift_witness