BT001N

mul_lt_mul_succ_left_nonzero

Stable · empty-context checked

Multiplication by a nonzero left factor strictly increases across a successor step.

Exact expanded PA statement

forall c a. ~(c = 0) -> exists r. r + S (c * a) = c * S a

Structural proof guide

Multiplication by a nonzero left factor strictly increases across a successor step.

Direct prerequisites: add_comm. The authored body proceeds by structural induction (1).

Proof neighborhood

Direct dependencies

BT0002 add_comm

Direct dependents

BT00QE succ_le_mul_of_two_le_right BT00R9 square_lt_successor_square BT00TY mul_lt_mul_right_nonzero

Formal native tactic body

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

  1. 0001induction c
  2. 0002intro a
  3. 0003intro hc
  4. 0004exfalso
  5. 0005apply hc
  6. 0006refl
  7. 0007intro a
  8. 0008intro hc
  9. 0009exists c
  10. 0010trans S (c + S c * a)
  11. 0011apply PA4
  12. 0012trans S (S c * a + c)
  13. 0013congr
  14. 0014apply add_comm
  15. 0015trans S c * a + S c
  16. 0016symm
  17. 0017apply PA4
  18. 0018symm
  19. 0019apply PA6