BT00TY

mul_lt_mul_right_nonzero

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Right multiplication by a nonzero natural preserves strict order.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall a b c. (exists bcf_lt_gap_mlmrn_source. bcf_lt_gap_mlmrn_source + S (a) = b) -> ~(c = 0) -> (exists bcf_lt_gap_mlmrn_result. bcf_lt_gap_mlmrn_result + S (a * c) = b * c)

Structural proof guide

Right multiplication by a nonzero natural preserves strict order.

Direct prerequisites: mul_comm, mul_lt_mul_succ_left_nonzero, mul_le_mul_right, lt_of_lt_of_le. The authored body proceeds by intermediate claims (5), equality transport (2).

Proof neighborhood

Direct dependencies

BT0006 mul_comm BT001N mul_lt_mul_succ_left_nonzero BT001M mul_le_mul_right BT001D lt_of_lt_of_le

Direct dependents

BT00U0 four_power_central_recurrence_step BT00U3 four_pow_central_seed_package

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

34 script commands · 7 reading checkpoints · 5 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
mul commmul lt mul succ left nonzeromul le mul rightlt of lt of le
01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro hab
  5. L5
    intro hc
02Establish hrawL6–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul lt mul succ left nonzero.

  1. L6
    have hraw : exists bcf_lt_gap_mlmrn_raw_step. bcf_lt_gap_mlmrn_raw_step + S (c * a) = c * S a
  2. L7
    specialize mul_lt_mul_succ_left_nonzero c
  3. L8
    specialize mul_lt_mul_succ_left_nonzero a
  4. L9
    apply mul_lt_mul_succ_left_nonzero
  5. L10
    exact hc
03Establish hleft_commL11–14

Establish this local claim before using it. It is not an additional assumption.

  1. L11
    have hleft_comm : c * a = a * c
  2. L12
    specialize mul_comm c
  3. L13
    specialize mul_comm a
  4. L14
    exact mul_comm
04Establish hright_commL15–20

Establish this local claim before using it. It is not an additional assumption.

  1. L15
    have hright_comm : c * S a = S a * c
  2. L16
    specialize mul_comm c
  3. L17
    specialize mul_comm (S a)
  4. L18
    exact mul_comm
  5. L19
    rewrite hleft_comm at hraw
  6. L20
    rewrite hright_comm at hraw
05Establish hstepL21–22

Establish this local claim before using it. It is not an additional assumption.

  1. L21
    have hstep : exists bcf_lt_gap_mlmrn_step. bcf_lt_gap_mlmrn_step + S (a * c) = S a * c
  2. L22
    exact hraw
06Establish htailL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul right.

  1. L23
    have htail : exists bcf_le_gap_mlmrn_tail. bcf_le_gap_mlmrn_tail + (S a * c) = b * c
  2. L24
    specialize mul_le_mul_right (S a)
  3. L25
    specialize mul_le_mul_right b
  4. L26
    specialize mul_le_mul_right c
  5. L27
    apply mul_le_mul_right
  6. L28
    exact hab
  7. L29
    specialize lt_of_lt_of_le (a * c)
  8. L30
    specialize lt_of_lt_of_le (S a * c)
  9. L31
    specialize lt_of_lt_of_le (b * c)
  10. L32
    apply lt_of_lt_of_le
07Use earlier factsL33–34

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L33
    exact hstep
  2. L34
    exact htail

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro hab
  5. 0005intro hc
  6. 0006have hraw : exists bcf_lt_gap_mlmrn_raw_step. bcf_lt_gap_mlmrn_raw_step + S (c * a) = c * S a
  7. 0007specialize mul_lt_mul_succ_left_nonzero c
  8. 0008specialize mul_lt_mul_succ_left_nonzero a
  9. 0009apply mul_lt_mul_succ_left_nonzero
  10. 0010exact hc
  11. 0011have hleft_comm : c * a = a * c
  12. 0012specialize mul_comm c
  13. 0013specialize mul_comm a
  14. 0014exact mul_comm
  15. 0015have hright_comm : c * S a = S a * c
  16. 0016specialize mul_comm c
  17. 0017specialize mul_comm (S a)
  18. 0018exact mul_comm
  19. 0019rewrite hleft_comm at hraw
  20. 0020rewrite hright_comm at hraw
  21. 0021have hstep : exists bcf_lt_gap_mlmrn_step. bcf_lt_gap_mlmrn_step + S (a * c) = S a * c
  22. 0022exact hraw
  23. 0023have htail : exists bcf_le_gap_mlmrn_tail. bcf_le_gap_mlmrn_tail + (S a * c) = b * c
  24. 0024specialize mul_le_mul_right (S a)
  25. 0025specialize mul_le_mul_right b
  26. 0026specialize mul_le_mul_right c
  27. 0027apply mul_le_mul_right
  28. 0028exact hab
  29. 0029specialize lt_of_lt_of_le (a * c)
  30. 0030specialize lt_of_lt_of_le (S a * c)
  31. 0031specialize lt_of_lt_of_le (b * c)
  32. 0032apply lt_of_lt_of_le
  33. 0033exact hstep
  34. 0034exact htail