BT00WE

ceil_div_six_budget_of_scaled_le

Alpha body-checked · checked-use disabled

A scaled lower bound cancels against the lower half of CeilDivSix.

Exact expanded PA statement

forall x k e. (((exists bcs_lower_gap_hj32_ceil_budget_source. bcs_lower_gap_hj32_ceil_budget_source + (x) = 6 * (e)) /\ exists bcs_upper_gap_hj32_ceil_budget_source. bcs_upper_gap_hj32_ceil_budget_source + S (6 * (e)) = (x) + 6)) -> (exists bqb_le_gap_hj32_ceil_budget_scaled. bqb_le_gap_hj32_ceil_budget_scaled + (6 * k) = (x)) -> (exists bqb_le_gap_hj32_ceil_budget_result. bqb_le_gap_hj32_ceil_budget_result + (k) = (e))

Structural proof guide

A scaled lower bound cancels against the lower half of CeilDivSix.

Direct prerequisites: le_trans, succ_ne_zero, mul_le_cancel_left_nonzero. The authored body proceeds by case analysis (1), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT000F le_trans BT000C succ_ne_zero BT00RD mul_le_cancel_left_nonzero

Direct dependents

BT00WP bertrand_h_root_32_from_total BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total

Formal native tactic body

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

  1. 0001intro x
  2. 0002intro k
  3. 0003intro e
  4. 0004intro hceiling
  5. 0005intro hscaled
  6. 0006cases hceiling
  7. 0007have hscaled_to_ceiling : exists bqb_le_gap_hj32_ceil_budget_chain. bqb_le_gap_hj32_ceil_budget_chain + (6 * k) = (6 * e)
  8. 0008specialize le_trans (6 * k)
  9. 0009specialize le_trans x
  10. 0010specialize le_trans (6 * e)
  11. 0011apply le_trans
  12. 0012exact hscaled
  13. 0013exact hceiling_left
  14. 0014specialize mul_le_cancel_left_nonzero 6
  15. 0015specialize mul_le_cancel_left_nonzero k
  16. 0016specialize mul_le_cancel_left_nonzero e
  17. 0017apply mul_le_cancel_left_nonzero
  18. 0018specialize succ_ne_zero 5
  19. 0019exact succ_ne_zero
  20. 0020exact hscaled_to_ceiling