BT001U

division_remainder_unique

Stable · empty-context checked

Bounded quotient-remainder decompositions have unique quotients and remainders.

Exact expanded PA statement

forall m n q r q2 r2. n = m * q + r -> (exists k. k + S r = m) -> n = m * q2 + r2 -> (exists k. k + S r2 = m) -> q = q2 /\ r = r2

Structural proof guide

Bounded quotient-remainder decompositions have unique quotients and remainders.

Direct prerequisites: zero_add, le_total, zero_or_succ, add_left_cancel, positive_quotient_gap_impossible. The authored body proceeds by case analysis (7), intermediate claims (1), equality transport (8).

Proof neighborhood

Direct dependencies

BT0000 zero_add BT000K le_total BT000Q zero_or_succ BT000V add_left_cancel BT001S positive_quotient_gap_impossible

Direct dependents

BT003B multiple_decidable_nonzero BT003W mod_eq_bounded_unique BT0042 beta_at_unique BT00S1 power_quotient_prefix_transport BT00SG division_remainder_successor_cases BT00SH division_successor_quotient_by_bit BT00SS prime_power_quotient_prefix_last_zero BT00XF division_zero_quotient_of_lt BT00XG division_double_quotient_bit BT00YC double_quotient_carry_prefix_entries_zero

Formal native tactic body

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

  1. 0001intro m
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro q2
  6. 0006intro r2
  7. 0007intro h1
  8. 0008intro hr
  9. 0009intro h2
  10. 0010intro hr2
  11. 0011have hsum : m * q + r = m * q2 + r2
  12. 0012trans n
  13. 0013symm
  14. 0014exact h1
  15. 0015exact h2
  16. 0016specialize le_total q
  17. 0017specialize le_total q2
  18. 0018cases le_total
  19. 0019cases le_total_left
  20. 0020specialize zero_or_succ x
  21. 0021cases zero_or_succ
  22. 0022rewrite zero_or_succ_left at le_total_left_witness
  23. 0023specialize zero_add q
  24. 0024rewrite zero_add at le_total_left_witness
  25. 0025split
  26. 0026exact le_total_left_witness
  27. 0027specialize add_left_cancel (m * q)
  28. 0028specialize add_left_cancel r
  29. 0029specialize add_left_cancel r2
  30. 0030apply add_left_cancel
  31. 0031rewrite <- le_total_left_witness at hsum
  32. 0032exact hsum
  33. 0033cases zero_or_succ_right
  34. 0034exfalso
  35. 0035specialize positive_quotient_gap_impossible m
  36. 0036specialize positive_quotient_gap_impossible q
  37. 0037specialize positive_quotient_gap_impossible q2
  38. 0038specialize positive_quotient_gap_impossible r
  39. 0039specialize positive_quotient_gap_impossible r2
  40. 0040specialize positive_quotient_gap_impossible x1
  41. 0041apply positive_quotient_gap_impossible
  42. 0042exact hr
  43. 0043rewrite zero_or_succ_right_witness at le_total_left_witness
  44. 0044exact le_total_left_witness
  45. 0045exact hsum
  46. 0046cases le_total_right
  47. 0047specialize zero_or_succ x
  48. 0048cases zero_or_succ
  49. 0049rewrite zero_or_succ_left at le_total_right_witness
  50. 0050specialize zero_add q2
  51. 0051rewrite zero_add at le_total_right_witness
  52. 0052split
  53. 0053symm
  54. 0054exact le_total_right_witness
  55. 0055specialize add_left_cancel (m * q)
  56. 0056specialize add_left_cancel r
  57. 0057specialize add_left_cancel r2
  58. 0058apply add_left_cancel
  59. 0059rewrite le_total_right_witness at hsum
  60. 0060exact hsum
  61. 0061cases zero_or_succ_right
  62. 0062exfalso
  63. 0063specialize positive_quotient_gap_impossible m
  64. 0064specialize positive_quotient_gap_impossible q2
  65. 0065specialize positive_quotient_gap_impossible q
  66. 0066specialize positive_quotient_gap_impossible r2
  67. 0067specialize positive_quotient_gap_impossible r
  68. 0068specialize positive_quotient_gap_impossible x1
  69. 0069apply positive_quotient_gap_impossible
  70. 0070exact hr2
  71. 0071rewrite zero_or_succ_right_witness at le_total_right_witness
  72. 0072exact le_total_right_witness
  73. 0073symm
  74. 0074exact hsum