BT00RH

canonical_double_triple_remainder_complement_budget

Alpha body-checked · checked-use disabled

Canonical remainder data yields and preserves the complement budget.

Exact expanded PA statement

forall n q r. (((2 * (n) = 3 * (q) + (r)) /\ exists bqb_remainder_gap_canonical_source. bqb_remainder_gap_canonical_source + S (r) = 3)) -> exists c. (((((q) + (c) = (n)) /\ exists bqb_budget_gap_canonical_result. bqb_budget_gap_canonical_result + 2 * (n) = 6 * (c))) /\ exists bqb_remainder_gap_canonical_preserved. bqb_remainder_gap_canonical_preserved + S r = 3)

Structural proof guide

Canonical remainder data yields and preserves the complement budget.

Direct prerequisites: double_triple_remainder_complement_budget. The authored body proceeds by case analysis (2), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT00RG double_triple_remainder_complement_budget

Direct dependents

BT00RJ floor_ceil_division_budget

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 hcanonical
  5. 0005cases hcanonical
  6. 0006have hbase : exists c. ((((q) + (c) = (n)) /\ exists bqb_budget_gap_canonical_base. bqb_budget_gap_canonical_base + 2 * (n) = 6 * (c)))
  7. 0007specialize double_triple_remainder_complement_budget n
  8. 0008specialize double_triple_remainder_complement_budget q
  9. 0009specialize double_triple_remainder_complement_budget r
  10. 0010apply double_triple_remainder_complement_budget
  11. 0011exact hcanonical_left
  12. 0012cases hbase
  13. 0013exists x
  14. 0014split
  15. 0015exact hbase_witness
  16. 0016exact hcanonical_right