BT002S

is_gcd_euclid_forward

Stable · empty-context checked

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

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 this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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