BT003A

eq_decidable

Stable · empty-context checked

Equality of natural numbers is constructively decidable.

Exact expanded PA statement

forall a b. a = b \/ ~(a = b)

Structural proof guide

Equality of natural numbers is constructively decidable.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

BT003B multiple_decidable_nonzero BT003C multiple_decidable BT003E factor_search_up_to BT003H prime_decidable BT00YM no_bertrand_central_prime_contribution_ranges BT0103 prime_contribution_cofactor_eq_one

Formal native tactic body

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

  1. 0001intro a
  2. 0002induction a
  3. 0003intro b
  4. 0004induction b
  5. 0005left
  6. 0006refl
  7. 0007right
  8. 0008intro h
  9. 0009apply PA1
  10. 0010symm
  11. 0011exact h
  12. 0012intro b
  13. 0013induction b
  14. 0014right
  15. 0015intro h
  16. 0016apply PA1
  17. 0017exact h
  18. 0018specialize IH b
  19. 0019cases IH
  20. 0020left
  21. 0021congr
  22. 0022exact IH_left
  23. 0023right
  24. 0024intro h
  25. 0025apply IH_right
  26. 0026apply PA2
  27. 0027exact h