BT00R4

square_six_shift_identity

Alpha body-checked · checked-use disabled

The six-step square increment is exactly six times 2*s+6.

Exact expanded PA statement

forall s. s * s + 6 * (2 * s + 6) = (s + 6) * (s + 6)

Structural proof guide

The six-step square increment is exactly six times 2*s+6.

Direct prerequisites: two_mul_eq_add_self, mul_add, add_mul, mul_comm, add_assoc. The authored body proceeds by intermediate claims (3), equality transport (1).

Proof neighborhood

Direct dependencies

BT00QU two_mul_eq_add_self BT0007 mul_add BT000B add_mul BT0006 mul_comm BT0003 add_assoc

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 s
  2. 0002have htwo : 2 * s = s + s
  3. 0003apply two_mul_eq_add_self
  4. 0004have hleft : 6 * (2 * s + 6) = (6 * s + 6 * s) + 6 * 6
  5. 0005trans 6 * (2 * s) + 6 * 6
  6. 0006apply mul_add
  7. 0007rewrite htwo
  8. 0008trans (6 * s + 6 * s) + 6 * 6
  9. 0009congr
  10. 0010apply mul_add
  11. 0011refl
  12. 0012refl
  13. 0013have hright : (s + 6) * (s + 6) = (s * s + 6 * s) + (6 * s + 6 * 6)
  14. 0014trans s * (s + 6) + 6 * (s + 6)
  15. 0015apply add_mul
  16. 0016trans (s * s + s * 6) + (6 * s + 6 * 6)
  17. 0017congr
  18. 0018apply mul_add
  19. 0019apply mul_add
  20. 0020trans (s * s + 6 * s) + (6 * s + 6 * 6)
  21. 0021congr
  22. 0022congr
  23. 0023refl
  24. 0024apply mul_comm
  25. 0025refl
  26. 0026refl
  27. 0027trans s * s + ((6 * s + 6 * s) + 6 * 6)
  28. 0028congr
  29. 0029refl
  30. 0030exact hleft
  31. 0031trans s * s + (6 * s + (6 * s + 6 * 6))
  32. 0032congr
  33. 0033refl
  34. 0034apply add_assoc
  35. 0035trans (s * s + 6 * s) + (6 * s + 6 * 6)
  36. 0036symm
  37. 0037apply add_assoc
  38. 0038symm
  39. 0039exact hright