BT00VS

odd_positive_prefix_predecessor_bound

Alpha body-checked · checked-use disabled

The positive prefix half of an odd successor is smaller.

Exact expanded PA statement

forall n k. S n = 2 * k + 1 -> (exists h. k = S h) -> (exists bcf_le_gap_boppb_result. bcf_le_gap_boppb_result + (S k) = n)

Structural proof guide

The positive prefix half of an odd successor is smaller.

Direct prerequisites: two_mul_eq_add_self, add_succ_left. The authored body proceeds by structural induction (1), case analysis (1).

Proof neighborhood

Direct dependencies

BT00QU two_mul_eq_add_self BT0001 add_succ_left

Direct dependents

BT00VV primorial_le_four_pow_bounded

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. 0002induction k
  3. 0003intro heq
  4. 0004intro hpositive
  5. 0005cases hpositive
  6. 0006exfalso
  7. 0007apply PA1
  8. 0008symm
  9. 0009exact hpositive_witness
  10. 0010intro heq
  11. 0011intro hpositive
  12. 0012exists k
  13. 0013apply PA2
  14. 0014trans 2 * S k + 1
  15. 0015simp [two_mul_eq_add_self, add_succ_left]
  16. 0016symm
  17. 0017exact heq