BT010A

two_lt_double_lower_six

Alpha body-checked · checked-use disabled

A natural above two has double at least three plus three.

Exact expanded PA statement

forall n. (exists bcf_lt_gap_b5rbtdls_positive. bcf_lt_gap_b5rbtdls_positive + S (2) = n) -> (exists bcf_le_gap_b5rbtdls_result. bcf_le_gap_b5rbtdls_result + (3 + 3) = n + n)

Structural proof guide

A natural above two has double at least three plus three.

Direct prerequisites: add_le_add_right, add_le_add_left, le_trans. The authored body proceeds by intermediate claims (2).

Proof neighborhood

Direct dependencies

BT0014 add_le_add_right BT0015 add_le_add_left BT000F le_trans

Direct dependents

BT010B floor_sqrt_two_le_of_two_lt BT010D floor_sqrt_three_mul_le_double

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro n
  2. 0002intro hpositive
  3. 0003have hleft : exists bcf_le_gap_b5rbtdls_left. bcf_le_gap_b5rbtdls_left + (3 + 3) = n + 3
  4. 0004specialize add_le_add_right 3
  5. 0005specialize add_le_add_right n
  6. 0006specialize add_le_add_right 3
  7. 0007apply add_le_add_right
  8. 0008exact hpositive
  9. 0009have hright : exists bcf_le_gap_b5rbtdls_right. bcf_le_gap_b5rbtdls_right + (n + 3) = n + n
  10. 0010specialize add_le_add_left 3
  11. 0011specialize add_le_add_left n
  12. 0012specialize add_le_add_left n
  13. 0013apply add_le_add_left
  14. 0014exact hpositive
  15. 0015specialize le_trans (3 + 3)
  16. 0016specialize le_trans (n + 3)
  17. 0017specialize le_trans (n + n)
  18. 0018apply le_trans
  19. 0019exact hleft
  20. 0020exact hright