BT000Q

zero_or_succ

Stable · empty-context checked

Every natural is either zero or the successor of a natural.

Exact expanded PA statement

forall n. n = 0 \/ exists k. n = S k

Structural proof guide

Every natural is either zero or the successor of a natural.

Direct prerequisites: none. The authored body proceeds by structural induction (1).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT001C le_eq_or_lt BT001O division_remainder_succ BT001P division_remainder_exists BT001U division_remainder_unique BT001W multiple_has_zero_remainder BT002F multiple_antisymm BT004M bounded_common_multiple_step BT006N prime_three BT00R1 ceil_div_six_total BT00RL prime_power_valuation_one_zero BT00T2 beta_pascal_zero_row_extend BT00T4 beta_pascal_row_step_extend BT00T6 beta_pascal_table_prefix_extend BT00TT choose_weighted_vertical BT00VV primorial_le_four_pow_bounded BT00YA prime_square_tail_of_two_three_range BT00YC double_quotient_carry_prefix_entries_zero BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients

Formal native tactic body

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

  1. 0001induction n
  2. 0002left
  3. 0003refl
  4. 0004right
  5. 0005exists n
  6. 0006refl