PA006S

mul_left_cancel_nonzero

Stable checked-use theorem · independently closed

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

Generated structural guide

A nonzero common left factor can be cancelled.

Use the direct prerequisites mul_eq_zero, mul_ne_zero, add_right_cancel, succ_ne_zero as previously established PA formulas.

The proof proceeds by structural induction (2), case analysis (1), intermediate claims (2), equality transport (4).

Referenced ingredients

PA0007 mul_eq_zero PA000S mul_ne_zero PA0012 add_right_cancel PA0005 succ_ne_zero

Proof neighborhood

Direct dependencies

PA0007 mul_eq_zero PA000S mul_ne_zero PA0012 add_right_cancel PA0005 succ_ne_zero

Direct dependents

PA006T odd_half_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  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