BT002G

factor_difference

Stable · empty-context checked

A common-factor difference is itself a multiple of that factor.

Exact expanded PA statement

forall c u v r. c * u = c * v + r -> exists w. r = c * w

Structural proof guide

A common-factor difference is itself a multiple of that factor.

Direct prerequisites: zero_add, add_eq_zero_right, add_right_cancel, add_assoc, add_comm. The authored body proceeds by structural induction (2), intermediate claims (2), equality transport (7).

Proof neighborhood

Direct dependencies

BT0000 zero_add BT000L add_eq_zero_right BT000U add_right_cancel BT0003 add_assoc BT0002 add_comm

Direct dependents

BT002H divides_remainder BT0037 common_divisor_divides_balanced_result BT00RD mul_le_cancel_left_nonzero

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro c
  2. 0002induction u
  3. 0003intro v
  4. 0004intro r
  5. 0005intro h
  6. 0006rewrite PA5 at h
  7. 0007have hr : r = 0
  8. 0008apply add_eq_zero_right
  9. 0009symm
  10. 0010exact h
  11. 0011exists 0
  12. 0012rewrite hr
  13. 0013rewrite PA5
  14. 0014refl
  15. 0015intro v
  16. 0016induction v
  17. 0017intro r
  18. 0018intro h
  19. 0019exists S u
  20. 0020rewrite PA5 at h
  21. 0021specialize zero_add r
  22. 0022rewrite zero_add at h
  23. 0023symm
  24. 0024exact h
  25. 0025intro r
  26. 0026intro h
  27. 0027have hred : c * u = c * v + r
  28. 0028specialize add_right_cancel (c * u)
  29. 0029specialize add_right_cancel (c * v + r)
  30. 0030specialize add_right_cancel c
  31. 0031apply add_right_cancel
  32. 0032rewrite PA6 at h
  33. 0033rewrite PA6 at h
  34. 0034trans (c * v + c) + r
  35. 0035exact h
  36. 0036trans c * v + (c + r)
  37. 0037apply add_assoc
  38. 0038trans c * v + (r + c)
  39. 0039congr
  40. 0040refl
  41. 0041apply add_comm
  42. 0042symm
  43. 0043apply add_assoc
  44. 0044specialize IH v
  45. 0045specialize IH r
  46. 0046apply IH
  47. 0047exact hred