BT001I

lt_not_le

Stable · empty-context checked

A strict inequality excludes the reverse weak inequality.

Exact expanded PA statement

forall a b. (exists k. k + S a = b) -> ~ (exists k. k + b = a)

Structural proof guide

A strict inequality excludes the reverse weak inequality.

Direct prerequisites: none. The authored body proceeds by structural induction (1), case analysis (2), intermediate claims (1), equality transport (5).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT001J le_not_lt BT00JD eisenstein_initial_segment_bit_count_functional BT00PR prime_strictly_above_decidable BT00QH power_valuation_successor_not_divides BT00RC floor_sqrt_monotone BT00SI valuation_threshold_bit_decides_power_divides BT00TC choose_functional BT00TD choose_out_of_range_zero BT00TE choose_zero BT00TI choose_succ_succ_of_lt BT00U4 four_pow_lt_mul_central_binom BT00VC choose_prime_divides_between BT00XG division_double_quotient_bit BT00Y6 central_binom_prime_square_tail_exponent_not_two_le BT00YA prime_square_tail_of_two_three_range BT010B floor_sqrt_two_le_of_two_lt BT010E division_quotient_lower_of_scaled_le BT010V no_bertrand_small_contribution_choice_le_double BT010W no_bertrand_middle_contribution_choice_le_selector BT010X no_bertrand_high_contribution_choice_eq_one BT0115 bertrand_eventually_closed_upper BT0117 factor_pair_has_small_member_below_square BT011A prime_le_twenty_two_cases BT011B nonzero_remainder_not_multiple BT011F prime_five BT011G prime_seven BT011H prime_thirteen BT011I prime_twenty_three BT011J prime_forty_three BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT0126 bertrand_upper_endpoint_factorization

Formal native tactic body

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

  1. 0001have hbad : forall z u v. ~(z = u + (v + S z))
  2. 0002intro z
  3. 0003induction z
  4. 0004intro u
  5. 0005intro v
  6. 0006intro hz
  7. 0007apply PA1
  8. 0008symm
  9. 0009rewrite PA4 at hz
  10. 0010rewrite PA4 at hz
  11. 0011exact hz
  12. 0012intro u
  13. 0013intro v
  14. 0014intro hz
  15. 0015specialize IH u
  16. 0016specialize IH v
  17. 0017apply IH
  18. 0018apply PA2
  19. 0019rewrite PA4 at hz
  20. 0020rewrite PA4 at hz
  21. 0021exact hz
  22. 0022intro a
  23. 0023intro b
  24. 0024intro hab
  25. 0025intro hba
  26. 0026cases hab
  27. 0027cases hba
  28. 0028specialize hbad a
  29. 0029specialize hbad x1
  30. 0030specialize hbad x
  31. 0031apply hbad
  32. 0032symm
  33. 0033rewrite <- hab_witness at hba_witness
  34. 0034exact hba_witness