BT00RF

ceil_div_six_le_of_upper

Alpha body-checked · checked-use disabled

Any six-multiple upper bound also bounds the ceiling quotient.

Exact expanded PA statement

forall x e c. (((exists bcs_lower_gap_upper_source. bcs_lower_gap_upper_source + (x) = 6 * (e)) /\ exists bcs_upper_gap_upper_source. bcs_upper_gap_upper_source + S (6 * (e)) = (x) + 6)) -> (exists k. k + x = 6 * c) -> exists k. k + e = c

Structural proof guide

Any six-multiple upper bound also bounds the ceiling quotient.

Direct prerequisites: le_or_lt, add_le_add_right, mul_le_mul_left, lt_of_lt_of_le, lt_irrefl_expanded. The authored body proceeds by case analysis (2), intermediate claims (5), equality transport (1).

Proof neighborhood

Direct dependencies

BT001G le_or_lt BT0014 add_le_add_right BT001L mul_le_mul_left BT001D lt_of_lt_of_le BT001B lt_irrefl_expanded

Direct dependents

BT00RI floor_ceil_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 x
  2. 0002intro e
  3. 0003intro c
  4. 0004intro he
  5. 0005intro hxc
  6. 0006cases he
  7. 0007specialize le_or_lt e
  8. 0008specialize le_or_lt c
  9. 0009cases le_or_lt
  10. 0010exact le_or_lt_left
  11. 0011exfalso
  12. 0012have hx6 : exists k. k + (x + 6) = 6 * c + 6
  13. 0013specialize add_le_add_right x
  14. 0014specialize add_le_add_right (6 * c)
  15. 0015specialize add_le_add_right 6
  16. 0016apply add_le_add_right
  17. 0017exact hxc
  18. 0018have hscaled : exists k. k + 6 * S c = 6 * e
  19. 0019apply mul_le_mul_left
  20. 0020exact le_or_lt_right
  21. 0021have hsucc : 6 * S c = 6 * c + 6
  22. 0022apply PA6
  23. 0023rewrite hsucc at hscaled
  24. 0024have hfirst : exists k. k + S (6 * e) = 6 * c + 6
  25. 0025specialize lt_of_lt_of_le (6 * e)
  26. 0026specialize lt_of_lt_of_le (x + 6)
  27. 0027specialize lt_of_lt_of_le (6 * c + 6)
  28. 0028apply lt_of_lt_of_le
  29. 0029exact he_right
  30. 0030exact hx6
  31. 0031have hloop : exists k. k + S (6 * e) = 6 * e
  32. 0032specialize lt_of_lt_of_le (6 * e)
  33. 0033specialize lt_of_lt_of_le (6 * c + 6)
  34. 0034specialize lt_of_lt_of_le (6 * e)
  35. 0035apply lt_of_lt_of_le
  36. 0036exact hfirst
  37. 0037exact hscaled
  38. 0038specialize lt_irrefl_expanded (6 * e)
  39. 0039apply lt_irrefl_expanded
  40. 0040exact hloop