EC0005

euclidean_two_step_quotient_nonzero

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 first-order arithmetic 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 27 exact native proof lines.

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

Proof neighborhood

Direct dependencies

lt_trans Stable theorem; checked-use authorized lt_irrefl_expanded Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized

Direct dependents

EC0006 euclidean_two_step_halving

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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