BT00R2

ceil_div_six_functional

Alpha body-checked · checked-use disabled

The two witness inequalities determine a unique ceiling quotient.

Exact expanded PA statement

forall x e f. (((exists bcs_lower_gap_functional_left. bcs_lower_gap_functional_left + (x) = 6 * (e)) /\ exists bcs_upper_gap_functional_left. bcs_upper_gap_functional_left + S (6 * (e)) = (x) + 6)) -> (((exists bcs_lower_gap_functional_right. bcs_lower_gap_functional_right + (x) = 6 * (f)) /\ exists bcs_upper_gap_functional_right. bcs_upper_gap_functional_right + S (6 * (f)) = (x) + 6)) -> e = f

Structural proof guide

The two witness inequalities determine a unique ceiling quotient.

Direct prerequisites: lt_trichotomy, add_le_add_right, mul_le_mul_left, lt_of_lt_of_le, lt_irrefl_expanded. The authored body proceeds by case analysis (4), intermediate claims (10), equality transport (2).

Proof neighborhood

Direct dependencies

BT001H lt_trichotomy BT0014 add_le_add_right BT001L mul_le_mul_left BT001D lt_of_lt_of_le BT001B lt_irrefl_expanded

Direct dependents

BT00R5 ceil_div_six_square_six_step

Formal native tactic body

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

  1. 0001intro x
  2. 0002intro e
  3. 0003intro f
  4. 0004intro he
  5. 0005intro hf
  6. 0006cases he
  7. 0007cases hf
  8. 0008specialize lt_trichotomy e
  9. 0009specialize lt_trichotomy f
  10. 0010cases lt_trichotomy
  11. 0011exact lt_trichotomy_left
  12. 0012cases lt_trichotomy_right
  13. 0013exfalso
  14. 0014have hx6 : exists k. k + (x + 6) = 6 * e + 6
  15. 0015specialize add_le_add_right x
  16. 0016specialize add_le_add_right (6 * e)
  17. 0017specialize add_le_add_right 6
  18. 0018apply add_le_add_right
  19. 0019exact he_left
  20. 0020have hscaled : exists k. k + 6 * S e = 6 * f
  21. 0021apply mul_le_mul_left
  22. 0022exact lt_trichotomy_right_left
  23. 0023have hsucce : 6 * S e = 6 * e + 6
  24. 0024apply PA6
  25. 0025rewrite hsucce at hscaled
  26. 0026have hfirst : exists k. k + S (6 * f) = 6 * e + 6
  27. 0027specialize lt_of_lt_of_le (6 * f)
  28. 0028specialize lt_of_lt_of_le (x + 6)
  29. 0029specialize lt_of_lt_of_le (6 * e + 6)
  30. 0030apply lt_of_lt_of_le
  31. 0031exact hf_right
  32. 0032exact hx6
  33. 0033have hloop : exists k. k + S (6 * f) = 6 * f
  34. 0034specialize lt_of_lt_of_le (6 * f)
  35. 0035specialize lt_of_lt_of_le (6 * e + 6)
  36. 0036specialize lt_of_lt_of_le (6 * f)
  37. 0037apply lt_of_lt_of_le
  38. 0038exact hfirst
  39. 0039exact hscaled
  40. 0040specialize lt_irrefl_expanded (6 * f)
  41. 0041apply lt_irrefl_expanded
  42. 0042exact hloop
  43. 0043exfalso
  44. 0044have hx6 : exists k. k + (x + 6) = 6 * f + 6
  45. 0045specialize add_le_add_right x
  46. 0046specialize add_le_add_right (6 * f)
  47. 0047specialize add_le_add_right 6
  48. 0048apply add_le_add_right
  49. 0049exact hf_left
  50. 0050have hscaled : exists k. k + 6 * S f = 6 * e
  51. 0051apply mul_le_mul_left
  52. 0052exact lt_trichotomy_right_right
  53. 0053have hsuccf : 6 * S f = 6 * f + 6
  54. 0054apply PA6
  55. 0055rewrite hsuccf at hscaled
  56. 0056have hfirst : exists k. k + S (6 * e) = 6 * f + 6
  57. 0057specialize lt_of_lt_of_le (6 * e)
  58. 0058specialize lt_of_lt_of_le (x + 6)
  59. 0059specialize lt_of_lt_of_le (6 * f + 6)
  60. 0060apply lt_of_lt_of_le
  61. 0061exact he_right
  62. 0062exact hx6
  63. 0063have hloop : exists k. k + S (6 * e) = 6 * e
  64. 0064specialize lt_of_lt_of_le (6 * e)
  65. 0065specialize lt_of_lt_of_le (6 * f + 6)
  66. 0066specialize lt_of_lt_of_le (6 * e)
  67. 0067apply lt_of_lt_of_le
  68. 0068exact hfirst
  69. 0069exact hscaled
  70. 0070specialize lt_irrefl_expanded (6 * e)
  71. 0071apply lt_irrefl_expanded
  72. 0072exact hloop