BT00Y8

division_quotient_one_of_bounds

Alpha body-checked · checked-use disabled

Bounds between one and two divisors force quotient one.

Exact expanded PA statement

forall d n. (exists bcf_le_gap_bdqob_lower. bcf_le_gap_bdqob_lower + (d) = n) -> (exists bcf_lt_gap_bdqob_upper. bcf_lt_gap_bdqob_upper + S (n) = d + d) -> exists r. (((n) = (d) * (1) + (r) /\ (exists bcf_lt_gap_bdqob_result_bound. bcf_lt_gap_bdqob_result_bound + S (r) = d)))

Structural proof guide

Bounds between one and two divisors force quotient one.

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

Proof neighborhood

Direct dependencies

BT0002 add_comm BT000A mul_one BT00XC add_lt_cancel_left

Direct dependents

BT00YB division_first_two_of_two_three_range

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 hlower
  4. 0004intro hupper
  5. 0005cases hlower
  6. 0006have hsum : d + x = n
  7. 0007trans x + d
  8. 0008apply add_comm
  9. 0009exact hlower_witness
  10. 0010have hremainder : exists bcf_lt_gap_bdqob_remainder. bcf_lt_gap_bdqob_remainder + S (x) = d
  11. 0011rewrite <- hsum at hupper
  12. 0012specialize add_lt_cancel_left d
  13. 0013specialize add_lt_cancel_left x
  14. 0014specialize add_lt_cancel_left d
  15. 0015apply add_lt_cancel_left
  16. 0016exact hupper
  17. 0017exists x
  18. 0018split
  19. 0019trans d + x
  20. 0020symm
  21. 0021exact hsum
  22. 0022specialize mul_one d
  23. 0023rewrite mul_one
  24. 0024refl
  25. 0025exact hremainder