PA0057

parity_cases

Stable checked-use theorem · independently closed

Every natural has a constructive even-or-odd witness.

Exact expanded PA statement

forall n. exists k. n = 2 * k \/ n = 2 * k + 1

Structural proof guide

Generated structural guide

Every natural has a constructive even-or-odd witness.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by structural induction (1), case analysis (2), equality transport (2), certified simplification (2), closed numeral normalization (1).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA005A even_successor_to_odd PA005C odd_successor_to_even PA0064 prime_ne_two_is_odd PA00BV arbitrary_gauss_lemma_complete PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00CA even_sum_parity_cases PA00CD odd_sum_parity_cases PA00CK odd_product_division_mod_two

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001induction n
  2. 0002exists 0
  3. 0003left
  4. 0004norm_num
  5. 0005cases IH
  6. 0006cases IH_witness
  7. 0007exists x
  8. 0008right
  9. 0009rewrite IH_witness_left
  10. 0010simp
  11. 0011exists x + 1
  12. 0012left
  13. 0013rewrite IH_witness_right
  14. 0014simp