BT00RG

double_triple_remainder_complement_budget

Alpha body-checked · checked-use disabled

The equation 2*n=3*q+r constructively yields q+c=n and 2*n<=6*c.

Exact expanded PA statement

forall n q r. 2 * n = 3 * q + r -> exists c. ((((q) + (c) = (n)) /\ exists bqb_budget_gap_strong_result. bqb_budget_gap_strong_result + 2 * (n) = 6 * (c)))

Structural proof guide

The equation 2*n=3*q+r constructively yields q+c=n and 2*n<=6*c.

Direct prerequisites: mul_le_mul_right, le_add_right, le_trans, succ_ne_zero, mul_le_cancel_left_nonzero, add_comm, mul_add, three_mul_eq_two_mul_add_self, add_assoc, add_left_cancel, add_le_add_right, mul_le_mul_left, mul_assoc. The authored body proceeds by case analysis (1), intermediate claims (18), equality transport (6), closed numeral normalization (2).

Proof neighborhood

Direct dependencies

BT001M mul_le_mul_right BT0013 le_add_right BT000F le_trans BT000C succ_ne_zero BT00RD mul_le_cancel_left_nonzero BT0002 add_comm BT0007 mul_add BT00RE three_mul_eq_two_mul_add_self BT0003 add_assoc BT000V add_left_cancel BT0014 add_le_add_right BT001L mul_le_mul_left BT0008 mul_assoc

Direct dependents

BT00RH canonical_double_triple_remainder_complement_budget

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro q
  3. 0003intro r
  4. 0004intro hdiv
  5. 0005have hcoeff : exists k. k + 2 = 3
  6. 0006exists 1
  7. 0007norm_num
  8. 0008have h23 : exists k. k + 2 * q = 3 * q
  9. 0009specialize mul_le_mul_right 2
  10. 0010specialize mul_le_mul_right 3
  11. 0011specialize mul_le_mul_right q
  12. 0012apply mul_le_mul_right
  13. 0013exact hcoeff
  14. 0014have h3r : exists k. k + 3 * q = 3 * q + r
  15. 0015apply le_add_right
  16. 0016have hpre : exists k. k + 2 * q = 3 * q + r
  17. 0017specialize le_trans (2 * q)
  18. 0018specialize le_trans (3 * q)
  19. 0019specialize le_trans (3 * q + r)
  20. 0020apply le_trans
  21. 0021exact h23
  22. 0022exact h3r
  23. 0023have h2n : exists k. k + 2 * q = 2 * n
  24. 0024rewrite hdiv
  25. 0025exact hpre
  26. 0026have htwo0 : ~(2 = 0)
  27. 0027intro hzero
  28. 0028specialize succ_ne_zero 1
  29. 0029apply succ_ne_zero
  30. 0030exact hzero
  31. 0031have hqn : exists k. k + q = n
  32. 0032specialize mul_le_cancel_left_nonzero 2
  33. 0033specialize mul_le_cancel_left_nonzero q
  34. 0034specialize mul_le_cancel_left_nonzero n
  35. 0035apply mul_le_cancel_left_nonzero
  36. 0036exact htwo0
  37. 0037exact h2n
  38. 0038cases hqn
  39. 0039have hcomp : q + x = n
  40. 0040trans x + q
  41. 0041apply add_comm
  42. 0042exact hqn_witness
  43. 0043have hbalance : 2 * q + 2 * x = 3 * q + r
  44. 0044trans 2 * (q + x)
  45. 0045symm
  46. 0046apply mul_add
  47. 0047rewrite hcomp
  48. 0048exact hdiv
  49. 0049have hthreeq : 3 * q = 2 * q + q
  50. 0050apply three_mul_eq_two_mul_add_self
  51. 0051have hbalance2 : 2 * q + 2 * x = 2 * q + (q + r)
  52. 0052trans 3 * q + r
  53. 0053exact hbalance
  54. 0054rewrite hthreeq
  55. 0055apply add_assoc
  56. 0056have hreduce : 2 * x = q + r
  57. 0057specialize add_left_cancel (2 * q)
  58. 0058specialize add_left_cancel (2 * x)
  59. 0059specialize add_left_cancel (q + r)
  60. 0060apply add_left_cancel
  61. 0061exact hbalance2
  62. 0062have hq2c : exists k. k + q = 2 * x
  63. 0063exists r
  64. 0064trans q + r
  65. 0065apply add_comm
  66. 0066symm
  67. 0067exact hreduce
  68. 0068have hplus : exists k. k + (q + x) = 2 * x + x
  69. 0069specialize add_le_add_right q
  70. 0070specialize add_le_add_right (2 * x)
  71. 0071specialize add_le_add_right x
  72. 0072apply add_le_add_right
  73. 0073exact hq2c
  74. 0074have hthreex : 3 * x = 2 * x + x
  75. 0075apply three_mul_eq_two_mul_add_self
  76. 0076have hn3c : exists k. k + n = 3 * x
  77. 0077rewrite <- hcomp
  78. 0078rewrite hthreex
  79. 0079exact hplus
  80. 0080have hscaled : exists k. k + 2 * n = 2 * (3 * x)
  81. 0081apply mul_le_mul_left
  82. 0082exact hn3c
  83. 0083have hfactor : 2 * (3 * x) = 6 * x
  84. 0084trans (2 * 3) * x
  85. 0085symm
  86. 0086apply mul_assoc
  87. 0087congr
  88. 0088norm_num
  89. 0089refl
  90. 0090exists x
  91. 0091split
  92. 0092exact hcomp
  93. 0093rewrite hfactor at hscaled
  94. 0094exact hscaled