BT0055

le_scaled_nonzero

Stable · empty-context checked

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

Scaling by a nonzero natural does not decrease a natural.

Direct prerequisites: one_le_of_ne_zero, mul_le_mul_right, one_mul. The authored body proceeds by intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT0010 one_le_of_ne_zero BT001M mul_le_mul_right BT0009 one_mul

Direct dependents

BT0057 beta_value_lt_scaled_base BT0058 new_value_lt_scaled_base

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 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