BT00R0

ceil_div_six_shift

Alpha body-checked · checked-use disabled

Ceiling by six commutes with adding an explicit multiple of six.

Exact expanded PA statement

forall x e k. (((exists bcs_lower_gap_shift_source. bcs_lower_gap_shift_source + (x) = 6 * (e)) /\ exists bcs_upper_gap_shift_source. bcs_upper_gap_shift_source + S (6 * (e)) = (x) + 6)) -> (((exists bcs_lower_gap_shift_target. bcs_lower_gap_shift_target + (x + 6 * k) = 6 * (e + k)) /\ exists bcs_upper_gap_shift_target. bcs_upper_gap_shift_target + S (6 * (e + k)) = (x + 6 * k) + 6))

Structural proof guide

Ceiling by six commutes with adding an explicit multiple of six.

Direct prerequisites: mul_add, add_assoc, add_comm, add_succ_left. The authored body proceeds by case analysis (3), intermediate claims (1), equality transport (4).

Proof neighborhood

Direct dependencies

BT0007 mul_add BT0003 add_assoc BT0002 add_comm BT0001 add_succ_left

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 k
  4. 0004intro h
  5. 0005have hmul : 6 * (e + k) = 6 * e + 6 * k
  6. 0006specialize mul_add 6
  7. 0007specialize mul_add e
  8. 0008specialize mul_add k
  9. 0009exact mul_add
  10. 0010cases h
  11. 0011split
  12. 0012cases h_left
  13. 0013exists x1
  14. 0014rewrite hmul
  15. 0015trans (x1 + x) + 6 * k
  16. 0016symm
  17. 0017apply add_assoc
  18. 0018rewrite h_left_witness
  19. 0019refl
  20. 0020cases h_right
  21. 0021exists x1
  22. 0022rewrite hmul
  23. 0023trans x1 + (S (6 * e) + 6 * k)
  24. 0024congr
  25. 0025refl
  26. 0026symm
  27. 0027apply add_succ_left
  28. 0028trans (x1 + S (6 * e)) + 6 * k
  29. 0029symm
  30. 0030apply add_assoc
  31. 0031rewrite h_right_witness
  32. 0032trans x + (6 + 6 * k)
  33. 0033apply add_assoc
  34. 0034trans x + (6 * k + 6)
  35. 0035congr
  36. 0036refl
  37. 0037apply add_comm
  38. 0038symm
  39. 0039apply add_assoc