BT00XC

add_lt_cancel_left

Alpha body-checked · checked-use disabled

A common left summand cancels from strict witness order.

Exact expanded PA statement

forall c a b. (exists bcf_lt_gap_b5altcl_source. bcf_lt_gap_b5altcl_source + S (c + a) = c + b) -> (exists bcf_lt_gap_b5altcl_result. bcf_lt_gap_b5altcl_result + S (a) = b)

Structural proof guide

A common left summand cancels from strict witness order.

Direct prerequisites: add_assoc, add_comm, add_left_cancel. The authored body proceeds by case analysis (1).

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT0002 add_comm BT000V add_left_cancel

Direct dependents

BT00XG division_double_quotient_bit BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds BT00YB division_first_two_of_two_three_range

Formal native tactic body

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

  1. 0001intro c
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hsource
  5. 0005cases hsource
  6. 0006exists x
  7. 0007specialize add_left_cancel c
  8. 0008specialize add_left_cancel (x + S a)
  9. 0009specialize add_left_cancel b
  10. 0010apply add_left_cancel
  11. 0011trans x + S (c + a)
  12. 0012trans c + S (x + a)
  13. 0013congr
  14. 0014refl
  15. 0015apply PA4
  16. 0016trans S (c + (x + a))
  17. 0017apply PA4
  18. 0018trans S (x + (c + a))
  19. 0019congr
  20. 0020trans (c + x) + a
  21. 0021symm
  22. 0022apply add_assoc
  23. 0023trans (x + c) + a
  24. 0024congr
  25. 0025apply add_comm
  26. 0026refl
  27. 0027apply add_assoc
  28. 0028symm
  29. 0029apply PA4
  30. 0030exact hsource_witness