EC0005

euclidean_two_step_quotient_nonzero

After one strict Euclidean decrease, the quotient of the next division cannot be zero.

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

∀ a. ∀ b. ∀ q. ∀ r. ∀ Q. ∀ t. EuclideanDivision(a,b,q,r) → EuclideanDivision(b,r,Q,t) → ¬Q = 0

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

Definition DAG

EuclideanDivision(a,b,q,r) · 2

Actual proof prerequisites

lt_trans · checked external prerequisitelt_irrefl_expanded · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall a b q r Q t. ((a = b * q + r /\ (exists ff_lt_ec_first_division. ff_lt_ec_first_division + S r = b))) -> ((b = r * Q + t /\ (exists ff_lt_ec_second_division. ff_lt_ec_second_division + S t = r))) -> ~(Q = 0)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

27 script commands · 7 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–8

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro Q
  6. L6
    intro t
  7. L7
    intro hfirst
  8. L8
    intro hsecond
02Separate the logical casesL9–10

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

  1. L9
    cases hfirst
  2. L10
    cases hsecond
03Fix variables and assumptionsL11–11

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

  1. L11
    intro hzero
04Establish hbtL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt irrefl expanded.

  1. L12
    have hbt : b = t
  2. L13
    trans (r * 0 + t)
  3. L14
    rewrite hzero at hsecond_left
  4. L15
    exact hsecond_left
  5. L16
    simp
  6. L17
    specialize zero_add t
  7. L18
    exact zero_add
  8. L19
    specialize lt_irrefl_expanded r
  9. L20
    apply lt_irrefl_expanded
  10. L21
    specialize lt_trans r
05Use earlier factsL22–24

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

  1. L22
    specialize lt_trans t
  2. L23
    specialize lt_trans r
  3. L24
    apply lt_trans
06Calculate and transport equalitiesL25–25

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

  1. L25
    rewrite hbt at hfirst_right
07Use earlier factsL26–27

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

  1. L26
    exact hfirst_right
  2. L27
    exact hsecond_right

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro Q
  6. 0006intro t
  7. 0007intro hfirst
  8. 0008intro hsecond
  9. 0009cases hfirst
  10. 0010cases hsecond
  11. 0011intro hzero
  12. 0012have hbt : b = t
  13. 0013trans (r * 0 + t)
  14. 0014rewrite hzero at hsecond_left
  15. 0015exact hsecond_left
  16. 0016simp
  17. 0017specialize zero_add t
  18. 0018exact zero_add
  19. 0019specialize lt_irrefl_expanded r
  20. 0020apply lt_irrefl_expanded
  21. 0021specialize lt_trans r
  22. 0022specialize lt_trans t
  23. 0023specialize lt_trans r
  24. 0024apply lt_trans
  25. 0025rewrite hbt at hfirst_right
  26. 0026exact hfirst_right
  27. 0027exact hsecond_right