BT0022

mul_left_cancel_nonzero

Stable · empty-context checked

A nonzero common left factor can be cancelled.

Exact expanded PA statement

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

Structural proof guide

A nonzero common left factor can be cancelled.

Direct prerequisites: mul_eq_zero, mul_ne_zero, add_right_cancel, succ_ne_zero. The authored body proceeds by structural induction (2), case analysis (1), intermediate claims (2), equality transport (4).

Proof neighborhood

Direct dependencies

BT000M mul_eq_zero BT0021 mul_ne_zero BT000U add_right_cancel BT000C succ_ne_zero

Direct dependents

BT002F multiple_antisymm BT003E factor_search_up_to BT003J proper_factor_lt BT00QN prime_power_successor_cancel_cofactor BT00RD mul_le_cancel_left_nonzero BT00U2 central_binom_four_weighted_of_recurrence

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 b
  3. 0003intro c
  4. 0004intro ha
  5. 0005intro h
  6. 0006have hz : a * c = 0
  7. 0007symm
  8. 0008rewrite PA5 at h
  9. 0009exact h
  10. 0010have factors : a = 0 \/ c = 0
  11. 0011specialize mul_eq_zero a
  12. 0012specialize mul_eq_zero c
  13. 0013apply mul_eq_zero
  14. 0014exact hz
  15. 0015cases factors
  16. 0016exfalso
  17. 0017apply ha
  18. 0018exact factors_left
  19. 0019symm
  20. 0020exact factors_right
  21. 0021intro c
  22. 0022induction c
  23. 0023intro ha
  24. 0024intro h
  25. 0025exfalso
  26. 0026specialize mul_ne_zero a
  27. 0027specialize mul_ne_zero (S b)
  28. 0028apply mul_ne_zero
  29. 0029exact ha
  30. 0030specialize succ_ne_zero b
  31. 0031exact succ_ne_zero
  32. 0032rewrite PA5 at h
  33. 0033exact h
  34. 0034intro ha
  35. 0035intro h
  36. 0036congr
  37. 0037apply IH
  38. 0038exact ha
  39. 0039apply add_right_cancel
  40. 0040rewrite PA6 at h
  41. 0041rewrite PA6 at h
  42. 0042exact h