BT00R9

square_lt_successor_square

Alpha body-checked · checked-use disabled

Every square is strictly below the next natural square.

Exact expanded PA statement

forall s. exists k. k + S (s * s) = S s * S s

Structural proof guide

Every square is strictly below the next natural square.

Direct prerequisites: le_succ_self, mul_le_mul_right, succ_ne_zero, mul_lt_mul_succ_left_nonzero, lt_of_le_of_lt. The authored body proceeds by intermediate claims (2).

Proof neighborhood

Direct dependencies

BT000X le_succ_self BT001M mul_le_mul_right BT000C succ_ne_zero BT001N mul_lt_mul_succ_left_nonzero BT001E lt_of_le_of_lt

Direct dependents

BT00RA floor_sqrt_total BT00X0 floor_sqrt_factorized_threshold_thirty_two

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 hleft : exists k. k + s * s = S s * s
  3. 0003apply mul_le_mul_right
  4. 0004apply le_succ_self
  5. 0005have hright : exists k. k + S (S s * s) = S s * S s
  6. 0006apply mul_lt_mul_succ_left_nonzero
  7. 0007intro hz
  8. 0008specialize succ_ne_zero s
  9. 0009apply succ_ne_zero
  10. 0010exact hz
  11. 0011specialize lt_of_le_of_lt (s * s)
  12. 0012specialize lt_of_le_of_lt (S s * s)
  13. 0013specialize lt_of_le_of_lt (S s * S s)
  14. 0014apply lt_of_le_of_lt
  15. 0015exact hleft
  16. 0016exact hright