BT00Y9

division_quotient_two_of_bounds

Alpha body-checked · checked-use disabled

Bounds between two and three divisors force quotient two.

Exact expanded PA statement

forall d n. (exists bcf_le_gap_bdqtb_lower. bcf_le_gap_bdqtb_lower + (d + d) = n) -> (exists bcf_lt_gap_bdqtb_upper. bcf_lt_gap_bdqtb_upper + S (n) = (d + d) + d) -> exists r. (((n) = (d) * (2) + (r) /\ (exists bcf_lt_gap_bdqtb_result_bound. bcf_lt_gap_bdqtb_result_bound + S (r) = d)))

Structural proof guide

Bounds between two and three divisors force quotient two.

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

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 + d) + x = n
  7. 0007trans x + (d + d)
  8. 0008apply add_comm
  9. 0009exact hlower_witness
  10. 0010have hremainder : exists bcf_lt_gap_bdqtb_remainder. bcf_lt_gap_bdqtb_remainder + S (x) = d
  11. 0011rewrite <- hsum at hupper
  12. 0012specialize add_lt_cancel_left (d + 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 + d) + x
  20. 0020symm
  21. 0021exact hsum
  22. 0022congr
  23. 0023rewrite PA6
  24. 0024specialize mul_one d
  25. 0025rewrite mul_one
  26. 0026refl
  27. 0027refl
  28. 0028exact hremainder