PA002N

le_scaled_nonzero

Stable checked-use theorem · independently closed

Scaling by a nonzero natural does not decrease a natural.

Exact expanded PA statement

forall C B. ~(C = 0) -> exists h. h + B = C * B

Structural proof guide

Generated structural guide

Scaling by a nonzero natural does not decrease a natural.

Use the direct prerequisites one_le_of_ne_zero, mul_le_mul_right, one_mul as previously established PA formulas.

The proof proceeds by intermediate claims (2), equality transport (1).

Referenced ingredients

PA002L one_le_of_ne_zero PA002M mul_le_mul_right PA000M one_mul

Proof neighborhood

Direct dependencies

PA002L one_le_of_ne_zero PA002M mul_le_mul_right PA000M one_mul

Direct dependents

PA002Q new_value_lt_scaled_base PA002T beta_value_lt_scaled_base

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 C
  2. 0002intro B
  3. 0003intro hC
  4. 0004have h1C : exists h. h + 1 = C
  5. 0005specialize one_le_of_ne_zero C
  6. 0006apply one_le_of_ne_zero
  7. 0007exact hC
  8. 0008have hscaled : exists h. h + 1 * B = C * B
  9. 0009specialize mul_le_mul_right 1
  10. 0010specialize mul_le_mul_right C
  11. 0011specialize mul_le_mul_right B
  12. 0012apply mul_le_mul_right
  13. 0013exact h1C
  14. 0014specialize one_mul B
  15. 0015rewrite one_mul at hscaled
  16. 0016exact hscaled