OAI/Algebra/DepthFive/CeilArithmetic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem335.ceilSqrt_zero line 7
  2. theorem OAI.Problem335.ceilSqrt_one line 10
  3. theorem OAI.Problem335.ceilSqrt_two line 13
  4. theorem OAI.Problem335.sqrt_le_ceilSqrt line 16
  5. theorem OAI.Problem335.ceilSqrt_le_sqrt_add_one line 20
  6. theorem OAI.Problem335.self_le_ceilSqrt_sq line 24
  7. theorem OAI.Problem335.ceilSqrt_pos line 31
  8. theorem OAI.Problem335.ceilSqrt_le_self line 34
  9. theorem OAI.Problem335.two_le_ceilSqrt line 43
  10. theorem OAI.Problem335.ceilSqrt_cast_le_real_sqrt_add_one line 50
  11. theorem OAI.Problem335.real_sqrt_le_ceilSqrt_cast line 59
  12. theorem OAI.Problem335.ceilDiv_le_iff line 64
  13. theorem OAI.Problem335.self_le_ceilDiv_mul line 71
  14. theorem OAI.Problem335.ceilDiv_le_self line 75
  15. theorem OAI.Problem335.ceilDiv_pos line 80
  16. theorem OAI.Problem335.ceilDiv_ceilSqrt_le line 87