BT00Y2

division_successor_quotient_divisor_le

Alpha body-checked · checked-use disabled

A division with successor quotient bounds its divisor by the dividend.

Exact expanded PA statement

forall d n q r. (((n) = (d) * (S q) + (r) /\ (exists bcf_lt_gap_b5ccsqdl_source_bound. bcf_lt_gap_b5ccsqdl_source_bound + S (r) = d))) -> (exists bcf_le_gap_b5ccsqdl_result. bcf_le_gap_b5ccsqdl_result + (d) = n)

Structural proof guide

A division with successor quotient bounds its divisor by the dividend.

Direct prerequisites: add_assoc, add_comm. The authored body proceeds by case analysis (1), intermediate claims (2), equality transport (2).

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT0002 add_comm

Direct dependents

BT00Y5 central_binom_prime_power_contribution_le_double

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro d
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hdivision
  6. 0006cases hdivision
  7. 0007exists d * q + r
  8. 0008rewrite hdivision_left
  9. 0009rewrite PA6
  10. 0010have hleft_assoc : (d * q + r) + d = d * q + (r + d)
  11. 0011apply add_assoc
  12. 0012have hright_assoc : (d * q + d) + r = d * q + (d + r)
  13. 0013apply add_assoc
  14. 0014trans d * q + (r + d)
  15. 0015exact hleft_assoc
  16. 0016trans d * q + (d + r)
  17. 0017congr
  18. 0018refl
  19. 0019apply add_comm
  20. 0020symm
  21. 0021exact hright_assoc