BT002S

is_gcd_euclid_forward

Stable checked-use theorem · independently kernel verified

A relational gcd of divisor and remainder is a gcd of dividend and divisor.

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 d a b q r. a = b * q + r -> (((exists x. b = d * x) /\ (exists y. r = d * y)) /\ forall c. (exists u. b = c * u) -> (exists v. r = c * v) -> exists w. d = c * w) -> (((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)

Structural proof guide

A relational gcd of divisor and remainder is a gcd of dividend and divisor.

Direct prerequisites: divides_remainder, divides_linear_step. The authored body proceeds by case analysis (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT002H divides_remainder BT002I divides_linear_step

Direct dependents

BT002U gcd_exists_up_to BT0034 gcd_balanced_bezout_exists_up_to

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

35 script commands · 7 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.

Named ingredients (2)
divides remainderdivides linear step
01Fix variables and assumptionsL1–7

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

  1. L1
    intro d
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro q
  5. L5
    intro r
  6. L6
    intro hstep
  7. L7
    intro hg
02Separate the logical casesL8–11

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

  1. L8
    cases hg
  2. L9
    cases hg_left
  3. L10
    split
  4. L11
    split
03Calculate and transport equalitiesL12–12

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

  1. L12
    rewrite hstep
04Use earlier factsL13–20

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

  1. L13
    specialize divides_linear_step d
  2. L14
    specialize divides_linear_step b
  3. L15
    specialize divides_linear_step q
  4. L16
    specialize divides_linear_step r
  5. L17
    apply divides_linear_step
  6. L18
    exact hg_left_left
  7. L19
    exact hg_left_right
  8. L20
    exact hg_left_left
05Fix variables and assumptionsL21–23

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

  1. L21
    intro c
  2. L22
    intro hca
  3. L23
    intro hcb
06Use earlier factsL24–33

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

  1. L24
    specialize hg_right c
  2. L25
    apply hg_right
  3. L26
    exact hcb
  4. L27
    specialize divides_remainder c
  5. L28
    specialize divides_remainder a
  6. L29
    specialize divides_remainder b
  7. L30
    specialize divides_remainder q
  8. L31
    specialize divides_remainder r
  9. L32
    apply divides_remainder
  10. L33
    exact hca
07Use earlier factsL34–35

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

  1. L34
    exact hcb
  2. L35
    exact hstep

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro d
  2. 0002intro a
  3. 0003intro b
  4. 0004intro q
  5. 0005intro r
  6. 0006intro hstep
  7. 0007intro hg
  8. 0008cases hg
  9. 0009cases hg_left
  10. 0010split
  11. 0011split
  12. 0012rewrite hstep
  13. 0013specialize divides_linear_step d
  14. 0014specialize divides_linear_step b
  15. 0015specialize divides_linear_step q
  16. 0016specialize divides_linear_step r
  17. 0017apply divides_linear_step
  18. 0018exact hg_left_left
  19. 0019exact hg_left_right
  20. 0020exact hg_left_left
  21. 0021intro c
  22. 0022intro hca
  23. 0023intro hcb
  24. 0024specialize hg_right c
  25. 0025apply hg_right
  26. 0026exact hcb
  27. 0027specialize divides_remainder c
  28. 0028specialize divides_remainder a
  29. 0029specialize divides_remainder b
  30. 0030specialize divides_remainder q
  31. 0031specialize divides_remainder r
  32. 0032apply divides_remainder
  33. 0033exact hca
  34. 0034exact hcb
  35. 0035exact hstep