BT00PW

le_mul_of_one_le_right

Alpha body-checked · checked-use disabled

A factor at least one makes right multiplication extensive.

Exact expanded PA statement

forall a b. (exists bpo_gap_right_factor. bpo_gap_right_factor + (1) = (b)) -> (exists bpo_gap_right_result. bpo_gap_right_result + (a) = (a * b))

Structural proof guide

A factor at least one makes right multiplication extensive.

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

Proof neighborhood

Direct dependencies

BT001L mul_le_mul_left BT000A mul_one

Direct dependents

BT00Q0 one_le_pow BT00SN pow_exponent_monotone_from_total BT00XJ pow_le_pow_of_exponent_le BT0115 bertrand_eventually_closed_upper

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