BT00TY

mul_lt_mul_right_nonzero

Alpha body-checked · checked-use disabled

Right multiplication by a nonzero natural preserves strict order.

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 this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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