BT010H

division_quotient_le_dividend

Alpha body-checked · checked-use disabled

The quotient by three is bounded by its doubled dividend.

Exact expanded PA statement

forall n q r. (((n + n) = (3) * (q) + (r) /\ (exists bcf_lt_gap_b5rbdqld_division_bound. bcf_lt_gap_b5rbdqld_division_bound + S (r) = 3))) -> (exists bcf_le_gap_b5rbdqld_result. bcf_le_gap_b5rbdqld_result + (q) = n + n)

Structural proof guide

The quotient by three is bounded by its doubled dividend.

Direct prerequisites: le_mul_of_one_le_left, le_add_right, le_trans. The authored body proceeds by case analysis (1), intermediate claims (4), equality transport (1), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT00PX le_mul_of_one_le_left BT0013 le_add_right BT000F le_trans

Direct dependents

BT010I third_quotient_double_gap_exists

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro q
  3. 0003intro r
  4. 0004intro hdivision
  5. 0005cases hdivision
  6. 0006have hone_three : exists bcf_le_gap_b5rbdqld_one_three. bcf_le_gap_b5rbdqld_one_three + (1) = 3
  7. 0007exists 2
  8. 0008norm_num
  9. 0009have hscaled : exists bcf_le_gap_b5rbdqld_scaled. bcf_le_gap_b5rbdqld_scaled + (q) = 3 * q
  10. 0010specialize le_mul_of_one_le_left 3
  11. 0011specialize le_mul_of_one_le_left q
  12. 0012apply le_mul_of_one_le_left
  13. 0013exact hone_three
  14. 0014have hadd : exists bcf_le_gap_b5rbdqld_added. bcf_le_gap_b5rbdqld_added + (3 * q) = 3 * q + r
  15. 0015specialize le_add_right (3 * q)
  16. 0016specialize le_add_right r
  17. 0017exact le_add_right
  18. 0018have hraw : exists bcf_le_gap_b5rbdqld_raw. bcf_le_gap_b5rbdqld_raw + (q) = 3 * q + r
  19. 0019specialize le_trans q
  20. 0020specialize le_trans (3 * q)
  21. 0021specialize le_trans (3 * q + r)
  22. 0022apply le_trans
  23. 0023exact hscaled
  24. 0024exact hadd
  25. 0025rewrite hdivision_left
  26. 0026exact hraw