BT00XV

double_quotient_carry_choice

Alpha body-checked · checked-use disabled

Each pair of doubled quotients has a constructive carry bit.

Exact expanded PA statement

forall p n b c d e l i. (forall bls_index_b5ccqc_left. (exists bls_gap_b5ccqc_left_bound. bls_gap_b5ccqc_left_bound + S (bls_index_b5ccqc_left) = (l)) -> exists bls_power_b5ccqc_left bls_quotient_b5ccqc_left bls_remainder_b5ccqc_left. ((exists bpvi_b_bls_b5ccqc_left_power bpvi_c_bls_b5ccqc_left_power. ((forall bpvi_i_bls_b5ccqc_left_power. (exists bpvi_repeat_gap_bls_b5ccqc_left_power. bpvi_repeat_gap_bls_b5ccqc_left_power + S bpvi_i_bls_b5ccqc_left_power = S bls_index_b5ccqc_left) -> (((exists bpvi_h_bls_b5ccqc_left_power_repeat. bpvi_h_bls_b5ccqc_left_power_repeat + S (p) = S ((S (bpvi_i_bls_b5ccqc_left_power)) * bpvi_c_bls_b5ccqc_left_power)) /\ exists bpvi_q_bls_b5ccqc_left_power_repeat. bpvi_b_bls_b5ccqc_left_power = bpvi_q_bls_b5ccqc_left_power_repeat * S ((S (bpvi_i_bls_b5ccqc_left_power)) * bpvi_c_bls_b5ccqc_left_power) + (p)))) /\ (exists bpvi_u_bls_b5ccqc_left_power bpvi_v_bls_b5ccqc_left_power. ((((exists bpvi_h_bls_b5ccqc_left_power_start. bpvi_h_bls_b5ccqc_left_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5ccqc_left_power)) /\ exists bpvi_q_bls_b5ccqc_left_power_start. bpvi_u_bls_b5ccqc_left_power = bpvi_q_bls_b5ccqc_left_power_start * S ((S (0)) * bpvi_v_bls_b5ccqc_left_power) + (1))) /\ ((((exists bpvi_h_bls_b5ccqc_left_power_terminal. bpvi_h_bls_b5ccqc_left_power_terminal + S (bls_power_b5ccqc_left) = S ((S (S bls_index_b5ccqc_left)) * bpvi_v_bls_b5ccqc_left_power)) /\ exists bpvi_q_bls_b5ccqc_left_power_terminal. bpvi_u_bls_b5ccqc_left_power = bpvi_q_bls_b5ccqc_left_power_terminal * S ((S (S bls_index_b5ccqc_left)) * bpvi_v_bls_b5ccqc_left_power) + (bls_power_b5ccqc_left))) /\ forall bpvi_j_bls_b5ccqc_left_power. (exists bpvi_product_gap_bls_b5ccqc_left_power. bpvi_product_gap_bls_b5ccqc_left_power + S bpvi_j_bls_b5ccqc_left_power = S bls_index_b5ccqc_left) -> exists bpvi_factor_bls_b5ccqc_left_power bpvi_partial_bls_b5ccqc_left_power bpvi_successor_bls_b5ccqc_left_power. ((((exists bpvi_h_bls_b5ccqc_left_power_factor. bpvi_h_bls_b5ccqc_left_power_factor + S (bpvi_factor_bls_b5ccqc_left_power) = S ((S (bpvi_j_bls_b5ccqc_left_power)) * bpvi_c_bls_b5ccqc_left_power)) /\ exists bpvi_q_bls_b5ccqc_left_power_factor. bpvi_b_bls_b5ccqc_left_power = bpvi_q_bls_b5ccqc_left_power_factor * S ((S (bpvi_j_bls_b5ccqc_left_power)) * bpvi_c_bls_b5ccqc_left_power) + (bpvi_factor_bls_b5ccqc_left_power))) /\ ((((exists bpvi_h_bls_b5ccqc_left_power_partial. bpvi_h_bls_b5ccqc_left_power_partial + S (bpvi_partial_bls_b5ccqc_left_power) = S ((S (bpvi_j_bls_b5ccqc_left_power)) * bpvi_v_bls_b5ccqc_left_power)) /\ exists bpvi_q_bls_b5ccqc_left_power_partial. bpvi_u_bls_b5ccqc_left_power = bpvi_q_bls_b5ccqc_left_power_partial * S ((S (bpvi_j_bls_b5ccqc_left_power)) * bpvi_v_bls_b5ccqc_left_power) + (bpvi_partial_bls_b5ccqc_left_power))) /\ ((((exists bpvi_h_bls_b5ccqc_left_power_successor. bpvi_h_bls_b5ccqc_left_power_successor + S (bpvi_successor_bls_b5ccqc_left_power) = S ((S (S bpvi_j_bls_b5ccqc_left_power)) * bpvi_v_bls_b5ccqc_left_power)) /\ exists bpvi_q_bls_b5ccqc_left_power_successor. bpvi_u_bls_b5ccqc_left_power = bpvi_q_bls_b5ccqc_left_power_successor * S ((S (S bpvi_j_bls_b5ccqc_left_power)) * bpvi_v_bls_b5ccqc_left_power) + (bpvi_successor_bls_b5ccqc_left_power))) /\ bpvi_successor_bls_b5ccqc_left_power = bpvi_partial_bls_b5ccqc_left_power * bpvi_factor_bls_b5ccqc_left_power)))))))) /\ ((((exists ff_h_bls_b5ccqc_left_quotient_entry. ff_h_bls_b5ccqc_left_quotient_entry + S (bls_quotient_b5ccqc_left) = S ((S (bls_index_b5ccqc_left)) * c)) /\ exists ff_q_bls_b5ccqc_left_quotient_entry. b = ff_q_bls_b5ccqc_left_quotient_entry * S ((S (bls_index_b5ccqc_left)) * c) + (bls_quotient_b5ccqc_left))) /\ ((n = bls_power_b5ccqc_left * bls_quotient_b5ccqc_left + bls_remainder_b5ccqc_left /\ exists bls_remainder_gap_b5ccqc_left_division. bls_remainder_gap_b5ccqc_left_division + S (bls_remainder_b5ccqc_left) = bls_power_b5ccqc_left))))) -> (forall bls_index_b5ccqc_right. (exists bls_gap_b5ccqc_right_bound. bls_gap_b5ccqc_right_bound + S (bls_index_b5ccqc_right) = (l)) -> exists bls_power_b5ccqc_right bls_quotient_b5ccqc_right bls_remainder_b5ccqc_right. ((exists bpvi_b_bls_b5ccqc_right_power bpvi_c_bls_b5ccqc_right_power. ((forall bpvi_i_bls_b5ccqc_right_power. (exists bpvi_repeat_gap_bls_b5ccqc_right_power. bpvi_repeat_gap_bls_b5ccqc_right_power + S bpvi_i_bls_b5ccqc_right_power = S bls_index_b5ccqc_right) -> (((exists bpvi_h_bls_b5ccqc_right_power_repeat. bpvi_h_bls_b5ccqc_right_power_repeat + S (p) = S ((S (bpvi_i_bls_b5ccqc_right_power)) * bpvi_c_bls_b5ccqc_right_power)) /\ exists bpvi_q_bls_b5ccqc_right_power_repeat. bpvi_b_bls_b5ccqc_right_power = bpvi_q_bls_b5ccqc_right_power_repeat * S ((S (bpvi_i_bls_b5ccqc_right_power)) * bpvi_c_bls_b5ccqc_right_power) + (p)))) /\ (exists bpvi_u_bls_b5ccqc_right_power bpvi_v_bls_b5ccqc_right_power. ((((exists bpvi_h_bls_b5ccqc_right_power_start. bpvi_h_bls_b5ccqc_right_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5ccqc_right_power)) /\ exists bpvi_q_bls_b5ccqc_right_power_start. bpvi_u_bls_b5ccqc_right_power = bpvi_q_bls_b5ccqc_right_power_start * S ((S (0)) * bpvi_v_bls_b5ccqc_right_power) + (1))) /\ ((((exists bpvi_h_bls_b5ccqc_right_power_terminal. bpvi_h_bls_b5ccqc_right_power_terminal + S (bls_power_b5ccqc_right) = S ((S (S bls_index_b5ccqc_right)) * bpvi_v_bls_b5ccqc_right_power)) /\ exists bpvi_q_bls_b5ccqc_right_power_terminal. bpvi_u_bls_b5ccqc_right_power = bpvi_q_bls_b5ccqc_right_power_terminal * S ((S (S bls_index_b5ccqc_right)) * bpvi_v_bls_b5ccqc_right_power) + (bls_power_b5ccqc_right))) /\ forall bpvi_j_bls_b5ccqc_right_power. (exists bpvi_product_gap_bls_b5ccqc_right_power. bpvi_product_gap_bls_b5ccqc_right_power + S bpvi_j_bls_b5ccqc_right_power = S bls_index_b5ccqc_right) -> exists bpvi_factor_bls_b5ccqc_right_power bpvi_partial_bls_b5ccqc_right_power bpvi_successor_bls_b5ccqc_right_power. ((((exists bpvi_h_bls_b5ccqc_right_power_factor. bpvi_h_bls_b5ccqc_right_power_factor + S (bpvi_factor_bls_b5ccqc_right_power) = S ((S (bpvi_j_bls_b5ccqc_right_power)) * bpvi_c_bls_b5ccqc_right_power)) /\ exists bpvi_q_bls_b5ccqc_right_power_factor. bpvi_b_bls_b5ccqc_right_power = bpvi_q_bls_b5ccqc_right_power_factor * S ((S (bpvi_j_bls_b5ccqc_right_power)) * bpvi_c_bls_b5ccqc_right_power) + (bpvi_factor_bls_b5ccqc_right_power))) /\ ((((exists bpvi_h_bls_b5ccqc_right_power_partial. bpvi_h_bls_b5ccqc_right_power_partial + S (bpvi_partial_bls_b5ccqc_right_power) = S ((S (bpvi_j_bls_b5ccqc_right_power)) * bpvi_v_bls_b5ccqc_right_power)) /\ exists bpvi_q_bls_b5ccqc_right_power_partial. bpvi_u_bls_b5ccqc_right_power = bpvi_q_bls_b5ccqc_right_power_partial * S ((S (bpvi_j_bls_b5ccqc_right_power)) * bpvi_v_bls_b5ccqc_right_power) + (bpvi_partial_bls_b5ccqc_right_power))) /\ ((((exists bpvi_h_bls_b5ccqc_right_power_successor. bpvi_h_bls_b5ccqc_right_power_successor + S (bpvi_successor_bls_b5ccqc_right_power) = S ((S (S bpvi_j_bls_b5ccqc_right_power)) * bpvi_v_bls_b5ccqc_right_power)) /\ exists bpvi_q_bls_b5ccqc_right_power_successor. bpvi_u_bls_b5ccqc_right_power = bpvi_q_bls_b5ccqc_right_power_successor * S ((S (S bpvi_j_bls_b5ccqc_right_power)) * bpvi_v_bls_b5ccqc_right_power) + (bpvi_successor_bls_b5ccqc_right_power))) /\ bpvi_successor_bls_b5ccqc_right_power = bpvi_partial_bls_b5ccqc_right_power * bpvi_factor_bls_b5ccqc_right_power)))))))) /\ ((((exists ff_h_bls_b5ccqc_right_quotient_entry. ff_h_bls_b5ccqc_right_quotient_entry + S (bls_quotient_b5ccqc_right) = S ((S (bls_index_b5ccqc_right)) * e)) /\ exists ff_q_bls_b5ccqc_right_quotient_entry. d = ff_q_bls_b5ccqc_right_quotient_entry * S ((S (bls_index_b5ccqc_right)) * e) + (bls_quotient_b5ccqc_right))) /\ ((n + n = bls_power_b5ccqc_right * bls_quotient_b5ccqc_right + bls_remainder_b5ccqc_right /\ exists bls_remainder_gap_b5ccqc_right_division. bls_remainder_gap_b5ccqc_right_division + S (bls_remainder_b5ccqc_right) = bls_power_b5ccqc_right))))) -> (exists bcf_lt_gap_b5ccqc_bound. bcf_lt_gap_b5ccqc_bound + S (i) = l) -> (exists q Q bit. (((exists fs_h_b5ccqc_result_left. fs_h_b5ccqc_result_left + S (q) = S ((S (i)) * c)) /\ exists fs_q_b5ccqc_result_left. b = fs_q_b5ccqc_result_left * S ((S (i)) * c) + (q))) /\ ((((exists fs_h_b5ccqc_result_right. fs_h_b5ccqc_result_right + S (Q) = S ((S (i)) * e)) /\ exists fs_q_b5ccqc_result_right. d = fs_q_b5ccqc_result_right * S ((S (i)) * e) + (Q))) /\ (((bit = 0 /\ Q = q + q) \/ (bit = 1 /\ Q = S (q + q))))))

Structural proof guide

Each pair of doubled quotients has a constructive carry bit.

Direct prerequisites: pow_functional, division_double_quotient_bit. The authored body proceeds by case analysis (11), intermediate claims (4), equality transport (2).

Proof neighborhood

Direct dependencies

BT0082 pow_functional BT00XG division_double_quotient_bit

Direct dependents

BT00XX double_quotient_carry_prefix_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 p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro l
  8. 0008intro i
  9. 0009intro hleft
  10. 0010intro hright
  11. 0011intro hi
  12. 0012have hleft_data : exists D q r. (exists bpvi_b_b5ccqc_left_power bpvi_c_b5ccqc_left_power. ((forall bpvi_i_b5ccqc_left_power. (exists bpvi_repeat_gap_b5ccqc_left_power. bpvi_repeat_gap_b5ccqc_left_power + S bpvi_i_b5ccqc_left_power = S i) -> (((exists bpvi_h_b5ccqc_left_power_repeat. bpvi_h_b5ccqc_left_power_repeat + S (p) = S ((S (bpvi_i_b5ccqc_left_power)) * bpvi_c_b5ccqc_left_power)) /\ exists bpvi_q_b5ccqc_left_power_repeat. bpvi_b_b5ccqc_left_power = bpvi_q_b5ccqc_left_power_repeat * S ((S (bpvi_i_b5ccqc_left_power)) * bpvi_c_b5ccqc_left_power) + (p)))) /\ (exists bpvi_u_b5ccqc_left_power bpvi_v_b5ccqc_left_power. ((((exists bpvi_h_b5ccqc_left_power_start. bpvi_h_b5ccqc_left_power_start + S (1) = S ((S (0)) * bpvi_v_b5ccqc_left_power)) /\ exists bpvi_q_b5ccqc_left_power_start. bpvi_u_b5ccqc_left_power = bpvi_q_b5ccqc_left_power_start * S ((S (0)) * bpvi_v_b5ccqc_left_power) + (1))) /\ ((((exists bpvi_h_b5ccqc_left_power_terminal. bpvi_h_b5ccqc_left_power_terminal + S (D) = S ((S (S i)) * bpvi_v_b5ccqc_left_power)) /\ exists bpvi_q_b5ccqc_left_power_terminal. bpvi_u_b5ccqc_left_power = bpvi_q_b5ccqc_left_power_terminal * S ((S (S i)) * bpvi_v_b5ccqc_left_power) + (D))) /\ forall bpvi_j_b5ccqc_left_power. (exists bpvi_product_gap_b5ccqc_left_power. bpvi_product_gap_b5ccqc_left_power + S bpvi_j_b5ccqc_left_power = S i) -> exists bpvi_factor_b5ccqc_left_power bpvi_partial_b5ccqc_left_power bpvi_successor_b5ccqc_left_power. ((((exists bpvi_h_b5ccqc_left_power_factor. bpvi_h_b5ccqc_left_power_factor + S (bpvi_factor_b5ccqc_left_power) = S ((S (bpvi_j_b5ccqc_left_power)) * bpvi_c_b5ccqc_left_power)) /\ exists bpvi_q_b5ccqc_left_power_factor. bpvi_b_b5ccqc_left_power = bpvi_q_b5ccqc_left_power_factor * S ((S (bpvi_j_b5ccqc_left_power)) * bpvi_c_b5ccqc_left_power) + (bpvi_factor_b5ccqc_left_power))) /\ ((((exists bpvi_h_b5ccqc_left_power_partial. bpvi_h_b5ccqc_left_power_partial + S (bpvi_partial_b5ccqc_left_power) = S ((S (bpvi_j_b5ccqc_left_power)) * bpvi_v_b5ccqc_left_power)) /\ exists bpvi_q_b5ccqc_left_power_partial. bpvi_u_b5ccqc_left_power = bpvi_q_b5ccqc_left_power_partial * S ((S (bpvi_j_b5ccqc_left_power)) * bpvi_v_b5ccqc_left_power) + (bpvi_partial_b5ccqc_left_power))) /\ ((((exists bpvi_h_b5ccqc_left_power_successor. bpvi_h_b5ccqc_left_power_successor + S (bpvi_successor_b5ccqc_left_power) = S ((S (S bpvi_j_b5ccqc_left_power)) * bpvi_v_b5ccqc_left_power)) /\ exists bpvi_q_b5ccqc_left_power_successor. bpvi_u_b5ccqc_left_power = bpvi_q_b5ccqc_left_power_successor * S ((S (S bpvi_j_b5ccqc_left_power)) * bpvi_v_b5ccqc_left_power) + (bpvi_successor_b5ccqc_left_power))) /\ bpvi_successor_b5ccqc_left_power = bpvi_partial_b5ccqc_left_power * bpvi_factor_b5ccqc_left_power)))))))) /\ ((((exists fs_h_b5ccqc_left_entry. fs_h_b5ccqc_left_entry + S (q) = S ((S (i)) * c)) /\ exists fs_q_b5ccqc_left_entry. b = fs_q_b5ccqc_left_entry * S ((S (i)) * c) + (q))) /\ (((n) = (D) * (q) + (r) /\ (exists bcf_lt_gap_b5ccqc_left_division_bound. bcf_lt_gap_b5ccqc_left_division_bound + S (r) = D))))
  13. 0013specialize hleft i
  14. 0014apply hleft
  15. 0015exact hi
  16. 0016cases hleft_data
  17. 0017cases hleft_data_witness
  18. 0018cases hleft_data_witness_witness
  19. 0019cases hleft_data_witness_witness_witness
  20. 0020cases hleft_data_witness_witness_witness_right
  21. 0021have hright_data : exists D q r. (exists bpvi_b_b5ccqc_right_power bpvi_c_b5ccqc_right_power. ((forall bpvi_i_b5ccqc_right_power. (exists bpvi_repeat_gap_b5ccqc_right_power. bpvi_repeat_gap_b5ccqc_right_power + S bpvi_i_b5ccqc_right_power = S i) -> (((exists bpvi_h_b5ccqc_right_power_repeat. bpvi_h_b5ccqc_right_power_repeat + S (p) = S ((S (bpvi_i_b5ccqc_right_power)) * bpvi_c_b5ccqc_right_power)) /\ exists bpvi_q_b5ccqc_right_power_repeat. bpvi_b_b5ccqc_right_power = bpvi_q_b5ccqc_right_power_repeat * S ((S (bpvi_i_b5ccqc_right_power)) * bpvi_c_b5ccqc_right_power) + (p)))) /\ (exists bpvi_u_b5ccqc_right_power bpvi_v_b5ccqc_right_power. ((((exists bpvi_h_b5ccqc_right_power_start. bpvi_h_b5ccqc_right_power_start + S (1) = S ((S (0)) * bpvi_v_b5ccqc_right_power)) /\ exists bpvi_q_b5ccqc_right_power_start. bpvi_u_b5ccqc_right_power = bpvi_q_b5ccqc_right_power_start * S ((S (0)) * bpvi_v_b5ccqc_right_power) + (1))) /\ ((((exists bpvi_h_b5ccqc_right_power_terminal. bpvi_h_b5ccqc_right_power_terminal + S (D) = S ((S (S i)) * bpvi_v_b5ccqc_right_power)) /\ exists bpvi_q_b5ccqc_right_power_terminal. bpvi_u_b5ccqc_right_power = bpvi_q_b5ccqc_right_power_terminal * S ((S (S i)) * bpvi_v_b5ccqc_right_power) + (D))) /\ forall bpvi_j_b5ccqc_right_power. (exists bpvi_product_gap_b5ccqc_right_power. bpvi_product_gap_b5ccqc_right_power + S bpvi_j_b5ccqc_right_power = S i) -> exists bpvi_factor_b5ccqc_right_power bpvi_partial_b5ccqc_right_power bpvi_successor_b5ccqc_right_power. ((((exists bpvi_h_b5ccqc_right_power_factor. bpvi_h_b5ccqc_right_power_factor + S (bpvi_factor_b5ccqc_right_power) = S ((S (bpvi_j_b5ccqc_right_power)) * bpvi_c_b5ccqc_right_power)) /\ exists bpvi_q_b5ccqc_right_power_factor. bpvi_b_b5ccqc_right_power = bpvi_q_b5ccqc_right_power_factor * S ((S (bpvi_j_b5ccqc_right_power)) * bpvi_c_b5ccqc_right_power) + (bpvi_factor_b5ccqc_right_power))) /\ ((((exists bpvi_h_b5ccqc_right_power_partial. bpvi_h_b5ccqc_right_power_partial + S (bpvi_partial_b5ccqc_right_power) = S ((S (bpvi_j_b5ccqc_right_power)) * bpvi_v_b5ccqc_right_power)) /\ exists bpvi_q_b5ccqc_right_power_partial. bpvi_u_b5ccqc_right_power = bpvi_q_b5ccqc_right_power_partial * S ((S (bpvi_j_b5ccqc_right_power)) * bpvi_v_b5ccqc_right_power) + (bpvi_partial_b5ccqc_right_power))) /\ ((((exists bpvi_h_b5ccqc_right_power_successor. bpvi_h_b5ccqc_right_power_successor + S (bpvi_successor_b5ccqc_right_power) = S ((S (S bpvi_j_b5ccqc_right_power)) * bpvi_v_b5ccqc_right_power)) /\ exists bpvi_q_b5ccqc_right_power_successor. bpvi_u_b5ccqc_right_power = bpvi_q_b5ccqc_right_power_successor * S ((S (S bpvi_j_b5ccqc_right_power)) * bpvi_v_b5ccqc_right_power) + (bpvi_successor_b5ccqc_right_power))) /\ bpvi_successor_b5ccqc_right_power = bpvi_partial_b5ccqc_right_power * bpvi_factor_b5ccqc_right_power)))))))) /\ ((((exists fs_h_b5ccqc_right_entry. fs_h_b5ccqc_right_entry + S (q) = S ((S (i)) * e)) /\ exists fs_q_b5ccqc_right_entry. d = fs_q_b5ccqc_right_entry * S ((S (i)) * e) + (q))) /\ (((n + n) = (D) * (q) + (r) /\ (exists bcf_lt_gap_b5ccqc_right_division_bound. bcf_lt_gap_b5ccqc_right_division_bound + S (r) = D))))
  22. 0022specialize hright i
  23. 0023apply hright
  24. 0024exact hi
  25. 0025cases hright_data
  26. 0026cases hright_data_witness
  27. 0027cases hright_data_witness_witness
  28. 0028cases hright_data_witness_witness_witness
  29. 0029cases hright_data_witness_witness_witness_right
  30. 0030have hpower_eq : x = x3
  31. 0031specialize pow_functional p
  32. 0032specialize pow_functional (S i)
  33. 0033specialize pow_functional x
  34. 0034specialize pow_functional x3
  35. 0035apply pow_functional
  36. 0036exact hleft_data_witness_witness_witness_left
  37. 0037exact hright_data_witness_witness_witness_left
  38. 0038rewrite <- hpower_eq at hright_data_witness_witness_witness_right_right
  39. 0039rewrite <- hpower_eq at hright_data_witness_witness_witness_right_right
  40. 0040have hcarry : x4 = x1 + x1 \/ x4 = S (x1 + x1)
  41. 0041specialize division_double_quotient_bit x
  42. 0042specialize division_double_quotient_bit n
  43. 0043specialize division_double_quotient_bit x1
  44. 0044specialize division_double_quotient_bit x2
  45. 0045specialize division_double_quotient_bit x4
  46. 0046specialize division_double_quotient_bit x5
  47. 0047apply division_double_quotient_bit
  48. 0048exact hleft_data_witness_witness_witness_right_right
  49. 0049exact hright_data_witness_witness_witness_right_right
  50. 0050cases hcarry
  51. 0051exists x1
  52. 0052exists x4
  53. 0053exists 0
  54. 0054split
  55. 0055exact hleft_data_witness_witness_witness_right_left
  56. 0056split
  57. 0057exact hright_data_witness_witness_witness_right_left
  58. 0058left
  59. 0059split
  60. 0060refl
  61. 0061exact hcarry_left
  62. 0062exists x1
  63. 0063exists x4
  64. 0064exists 1
  65. 0065split
  66. 0066exact hleft_data_witness_witness_witness_right_left
  67. 0067split
  68. 0068exact hright_data_witness_witness_witness_right_left
  69. 0069right
  70. 0070split
  71. 0071refl
  72. 0072exact hcarry_right