BT00PX

le_mul_of_one_le_left

Alpha body-checked · checked-use disabled

A factor at least one makes left multiplication extensive.

Exact expanded PA statement

forall a b. (exists bpo_gap_left_factor. bpo_gap_left_factor + (1) = (a)) -> (exists bpo_gap_left_result. bpo_gap_left_result + (b) = (a * b))

Structural proof guide

A factor at least one makes left multiplication extensive.

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

Proof neighborhood

Direct dependencies

BT001M mul_le_mul_right BT0009 one_mul

Direct dependents

BT010H division_quotient_le_dividend BT0111 no_bertrand_middle_contribution_interval_le_four_pow

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. 0002intro b
  3. 0003intro ha
  4. 0004have hscaled : exists k. k + 1 * b = a * b
  5. 0005specialize mul_le_mul_right 1
  6. 0006specialize mul_le_mul_right a
  7. 0007specialize mul_le_mul_right b
  8. 0008apply mul_le_mul_right
  9. 0009exact ha
  10. 0010specialize one_mul b
  11. 0011rewrite one_mul at hscaled
  12. 0012exact hscaled