BT00RD

mul_le_cancel_left_nonzero

Alpha body-checked · checked-use disabled

Witness order cancels a common nonzero left multiplier.

Exact expanded PA statement

forall c a b. ~(c = 0) -> (exists k. k + c * a = c * b) -> exists k. k + a = b

Structural proof guide

Witness order cancels a common nonzero left multiplier.

Direct prerequisites: add_comm, factor_difference, mul_left_cancel_nonzero, mul_add. The authored body proceeds by case analysis (2), intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT0002 add_comm BT002G factor_difference BT0022 mul_left_cancel_nonzero BT0007 mul_add

Direct dependents

BT00RG double_triple_remainder_complement_budget BT00VK central_binom_strong_upper_step BT00VP central_binom_odd_middle_le_four_pow BT00WE ceil_div_six_budget_of_scaled_le

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 hc
  5. 0005intro hle
  6. 0006cases hle
  7. 0007have heq : c * b = c * a + x
  8. 0008trans x + c * a
  9. 0009symm
  10. 0010exact hle_witness
  11. 0011apply add_comm
  12. 0012have hfactor : exists w. x = c * w
  13. 0013specialize factor_difference c
  14. 0014specialize factor_difference b
  15. 0015specialize factor_difference a
  16. 0016specialize factor_difference x
  17. 0017apply factor_difference
  18. 0018exact heq
  19. 0019cases hfactor
  20. 0020exists x1
  21. 0021specialize mul_left_cancel_nonzero c
  22. 0022specialize mul_left_cancel_nonzero (x1 + a)
  23. 0023specialize mul_left_cancel_nonzero b
  24. 0024apply mul_left_cancel_nonzero
  25. 0025exact hc
  26. 0026trans c * x1 + c * a
  27. 0027apply mul_add
  28. 0028rewrite <- hfactor_witness
  29. 0029exact hle_witness