BT010I

third_quotient_double_gap_exists

Alpha body-checked · checked-use disabled

The third quotient has an exact additive gap to the doubled input.

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 h. q + h = n + n

Structural proof guide

The third quotient has an exact additive gap to the doubled input.

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

Proof neighborhood

Direct dependencies

BT0002 add_comm BT010H division_quotient_le_dividend

Direct dependents

BT010J floor_third_double_gap_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 n
  2. 0002intro q
  3. 0003intro r
  4. 0004intro hdivision
  5. 0005have hbound : exists bcf_le_gap_b5rbdqld_result. bcf_le_gap_b5rbdqld_result + (q) = n + n
  6. 0006specialize division_quotient_le_dividend n
  7. 0007specialize division_quotient_le_dividend q
  8. 0008specialize division_quotient_le_dividend r
  9. 0009apply division_quotient_le_dividend
  10. 0010exact hdivision
  11. 0011cases hbound
  12. 0012exists x
  13. 0013specialize add_comm q
  14. 0014specialize add_comm x
  15. 0015rewrite add_comm
  16. 0016exact hbound_witness