BT00QV

pow_mul_base

Alpha body-checked · checked-use disabled

A relational power of a product is the product of the powers.

Exact expanded PA statement

forall a b e x y z. (exists ff_b_bie_mul_left ff_c_bie_mul_left. ((forall ff_i_bie_mul_left_repeat. (exists ff_lt_bie_mul_left_repeat_bound. ff_lt_bie_mul_left_repeat_bound + S ff_i_bie_mul_left_repeat = e) -> (((exists ff_h_bie_mul_left_repeat_decoded. ff_h_bie_mul_left_repeat_decoded + S (a) = S ((S (ff_i_bie_mul_left_repeat)) * ff_c_bie_mul_left)) /\ exists ff_q_bie_mul_left_repeat_decoded. ff_b_bie_mul_left = ff_q_bie_mul_left_repeat_decoded * S ((S (ff_i_bie_mul_left_repeat)) * ff_c_bie_mul_left) + (a)))) /\ (exists ff_u_bie_mul_left_product ff_v_bie_mul_left_product. ((((exists ff_h_bie_mul_left_product_start. ff_h_bie_mul_left_product_start + S (1) = S ((S (0)) * ff_v_bie_mul_left_product)) /\ exists ff_q_bie_mul_left_product_start. ff_u_bie_mul_left_product = ff_q_bie_mul_left_product_start * S ((S (0)) * ff_v_bie_mul_left_product) + (1))) /\ ((((exists ff_h_bie_mul_left_product_terminal. ff_h_bie_mul_left_product_terminal + S (x) = S ((S (e)) * ff_v_bie_mul_left_product)) /\ exists ff_q_bie_mul_left_product_terminal. ff_u_bie_mul_left_product = ff_q_bie_mul_left_product_terminal * S ((S (e)) * ff_v_bie_mul_left_product) + (x))) /\ forall ff_i_bie_mul_left_product. (exists ff_lt_bie_mul_left_product_bound. ff_lt_bie_mul_left_product_bound + S ff_i_bie_mul_left_product = e) -> exists ff_p_bie_mul_left_product ff_r_bie_mul_left_product ff_s_bie_mul_left_product. ((((exists ff_h_bie_mul_left_product_factor. ff_h_bie_mul_left_product_factor + S (ff_p_bie_mul_left_product) = S ((S (ff_i_bie_mul_left_product)) * ff_c_bie_mul_left)) /\ exists ff_q_bie_mul_left_product_factor. ff_b_bie_mul_left = ff_q_bie_mul_left_product_factor * S ((S (ff_i_bie_mul_left_product)) * ff_c_bie_mul_left) + (ff_p_bie_mul_left_product))) /\ ((((exists ff_h_bie_mul_left_product_partial. ff_h_bie_mul_left_product_partial + S (ff_r_bie_mul_left_product) = S ((S (ff_i_bie_mul_left_product)) * ff_v_bie_mul_left_product)) /\ exists ff_q_bie_mul_left_product_partial. ff_u_bie_mul_left_product = ff_q_bie_mul_left_product_partial * S ((S (ff_i_bie_mul_left_product)) * ff_v_bie_mul_left_product) + (ff_r_bie_mul_left_product))) /\ ((((exists ff_h_bie_mul_left_product_successor. ff_h_bie_mul_left_product_successor + S (ff_s_bie_mul_left_product) = S ((S (S ff_i_bie_mul_left_product)) * ff_v_bie_mul_left_product)) /\ exists ff_q_bie_mul_left_product_successor. ff_u_bie_mul_left_product = ff_q_bie_mul_left_product_successor * S ((S (S ff_i_bie_mul_left_product)) * ff_v_bie_mul_left_product) + (ff_s_bie_mul_left_product))) /\ ff_s_bie_mul_left_product = ff_r_bie_mul_left_product * ff_p_bie_mul_left_product)))))))) -> (exists ff_b_bie_mul_right ff_c_bie_mul_right. ((forall ff_i_bie_mul_right_repeat. (exists ff_lt_bie_mul_right_repeat_bound. ff_lt_bie_mul_right_repeat_bound + S ff_i_bie_mul_right_repeat = e) -> (((exists ff_h_bie_mul_right_repeat_decoded. ff_h_bie_mul_right_repeat_decoded + S (b) = S ((S (ff_i_bie_mul_right_repeat)) * ff_c_bie_mul_right)) /\ exists ff_q_bie_mul_right_repeat_decoded. ff_b_bie_mul_right = ff_q_bie_mul_right_repeat_decoded * S ((S (ff_i_bie_mul_right_repeat)) * ff_c_bie_mul_right) + (b)))) /\ (exists ff_u_bie_mul_right_product ff_v_bie_mul_right_product. ((((exists ff_h_bie_mul_right_product_start. ff_h_bie_mul_right_product_start + S (1) = S ((S (0)) * ff_v_bie_mul_right_product)) /\ exists ff_q_bie_mul_right_product_start. ff_u_bie_mul_right_product = ff_q_bie_mul_right_product_start * S ((S (0)) * ff_v_bie_mul_right_product) + (1))) /\ ((((exists ff_h_bie_mul_right_product_terminal. ff_h_bie_mul_right_product_terminal + S (y) = S ((S (e)) * ff_v_bie_mul_right_product)) /\ exists ff_q_bie_mul_right_product_terminal. ff_u_bie_mul_right_product = ff_q_bie_mul_right_product_terminal * S ((S (e)) * ff_v_bie_mul_right_product) + (y))) /\ forall ff_i_bie_mul_right_product. (exists ff_lt_bie_mul_right_product_bound. ff_lt_bie_mul_right_product_bound + S ff_i_bie_mul_right_product = e) -> exists ff_p_bie_mul_right_product ff_r_bie_mul_right_product ff_s_bie_mul_right_product. ((((exists ff_h_bie_mul_right_product_factor. ff_h_bie_mul_right_product_factor + S (ff_p_bie_mul_right_product) = S ((S (ff_i_bie_mul_right_product)) * ff_c_bie_mul_right)) /\ exists ff_q_bie_mul_right_product_factor. ff_b_bie_mul_right = ff_q_bie_mul_right_product_factor * S ((S (ff_i_bie_mul_right_product)) * ff_c_bie_mul_right) + (ff_p_bie_mul_right_product))) /\ ((((exists ff_h_bie_mul_right_product_partial. ff_h_bie_mul_right_product_partial + S (ff_r_bie_mul_right_product) = S ((S (ff_i_bie_mul_right_product)) * ff_v_bie_mul_right_product)) /\ exists ff_q_bie_mul_right_product_partial. ff_u_bie_mul_right_product = ff_q_bie_mul_right_product_partial * S ((S (ff_i_bie_mul_right_product)) * ff_v_bie_mul_right_product) + (ff_r_bie_mul_right_product))) /\ ((((exists ff_h_bie_mul_right_product_successor. ff_h_bie_mul_right_product_successor + S (ff_s_bie_mul_right_product) = S ((S (S ff_i_bie_mul_right_product)) * ff_v_bie_mul_right_product)) /\ exists ff_q_bie_mul_right_product_successor. ff_u_bie_mul_right_product = ff_q_bie_mul_right_product_successor * S ((S (S ff_i_bie_mul_right_product)) * ff_v_bie_mul_right_product) + (ff_s_bie_mul_right_product))) /\ ff_s_bie_mul_right_product = ff_r_bie_mul_right_product * ff_p_bie_mul_right_product)))))))) -> (exists pa_b_bie_mul_product pa_c_bie_mul_product. ((forall pa_i_bie_mul_product_repeat. (exists pa_lt_bie_mul_product_repeat_bound. pa_lt_bie_mul_product_repeat_bound + S pa_i_bie_mul_product_repeat = e) -> (((exists pa_h_bie_mul_product_repeat_decoded. pa_h_bie_mul_product_repeat_decoded + S (a * b) = S ((S (pa_i_bie_mul_product_repeat)) * pa_c_bie_mul_product)) /\ exists pa_q_bie_mul_product_repeat_decoded. pa_b_bie_mul_product = pa_q_bie_mul_product_repeat_decoded * S ((S (pa_i_bie_mul_product_repeat)) * pa_c_bie_mul_product) + (a * b)))) /\ (exists pa_u_bie_mul_product_product pa_v_bie_mul_product_product. ((((exists pa_h_bie_mul_product_product_start. pa_h_bie_mul_product_product_start + S (1) = S ((S (0)) * pa_v_bie_mul_product_product)) /\ exists pa_q_bie_mul_product_product_start. pa_u_bie_mul_product_product = pa_q_bie_mul_product_product_start * S ((S (0)) * pa_v_bie_mul_product_product) + (1))) /\ ((((exists pa_h_bie_mul_product_product_terminal. pa_h_bie_mul_product_product_terminal + S (z) = S ((S (e)) * pa_v_bie_mul_product_product)) /\ exists pa_q_bie_mul_product_product_terminal. pa_u_bie_mul_product_product = pa_q_bie_mul_product_product_terminal * S ((S (e)) * pa_v_bie_mul_product_product) + (z))) /\ forall pa_i_bie_mul_product_product. (exists pa_lt_bie_mul_product_product_bound. pa_lt_bie_mul_product_product_bound + S pa_i_bie_mul_product_product = e) -> exists pa_p_bie_mul_product_product pa_r_bie_mul_product_product pa_s_bie_mul_product_product. ((((exists pa_h_bie_mul_product_product_factor. pa_h_bie_mul_product_product_factor + S (pa_p_bie_mul_product_product) = S ((S (pa_i_bie_mul_product_product)) * pa_c_bie_mul_product)) /\ exists pa_q_bie_mul_product_product_factor. pa_b_bie_mul_product = pa_q_bie_mul_product_product_factor * S ((S (pa_i_bie_mul_product_product)) * pa_c_bie_mul_product) + (pa_p_bie_mul_product_product))) /\ ((((exists pa_h_bie_mul_product_product_partial. pa_h_bie_mul_product_product_partial + S (pa_r_bie_mul_product_product) = S ((S (pa_i_bie_mul_product_product)) * pa_v_bie_mul_product_product)) /\ exists pa_q_bie_mul_product_product_partial. pa_u_bie_mul_product_product = pa_q_bie_mul_product_product_partial * S ((S (pa_i_bie_mul_product_product)) * pa_v_bie_mul_product_product) + (pa_r_bie_mul_product_product))) /\ ((((exists pa_h_bie_mul_product_product_successor. pa_h_bie_mul_product_product_successor + S (pa_s_bie_mul_product_product) = S ((S (S pa_i_bie_mul_product_product)) * pa_v_bie_mul_product_product)) /\ exists pa_q_bie_mul_product_product_successor. pa_u_bie_mul_product_product = pa_q_bie_mul_product_product_successor * S ((S (S pa_i_bie_mul_product_product)) * pa_v_bie_mul_product_product) + (pa_s_bie_mul_product_product))) /\ pa_s_bie_mul_product_product = pa_r_bie_mul_product_product * pa_p_bie_mul_product_product)))))))) -> z = x * y

Structural proof guide

A relational power of a product is the product of the powers.

Direct prerequisites: pow_zero, pow_successor_decompose, mul_one, mul_assoc, mul_comm. The authored body proceeds by structural induction (1), case analysis (6), intermediate claims (7), equality transport (5).

Proof neighborhood

Direct dependencies

BT0081 pow_zero BT0083 pow_successor_decompose BT000A mul_one BT0008 mul_assoc BT0006 mul_comm

Direct dependents

BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WP bertrand_h_root_32_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_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 a
  2. 0002intro b
  3. 0003intro e
  4. 0004induction e
  5. 0005intro x
  6. 0006intro y
  7. 0007intro z
  8. 0008intro hx
  9. 0009intro hy
  10. 0010intro hz
  11. 0011have hx1 : x = 1
  12. 0012specialize pow_zero a
  13. 0013specialize pow_zero 0
  14. 0014specialize pow_zero x
  15. 0015apply pow_zero
  16. 0016refl
  17. 0017exact hx
  18. 0018have hy1 : y = 1
  19. 0019specialize pow_zero b
  20. 0020specialize pow_zero 0
  21. 0021specialize pow_zero y
  22. 0022apply pow_zero
  23. 0023refl
  24. 0024exact hy
  25. 0025have hz1 : z = 1
  26. 0026specialize pow_zero (a * b)
  27. 0027specialize pow_zero 0
  28. 0028specialize pow_zero z
  29. 0029apply pow_zero
  30. 0030refl
  31. 0031exact hz
  32. 0032rewrite hz1
  33. 0033rewrite hx1
  34. 0034rewrite hy1
  35. 0035symm
  36. 0036specialize mul_one 1
  37. 0037exact mul_one
  38. 0038intro x
  39. 0039intro y
  40. 0040intro z
  41. 0041intro hx
  42. 0042intro hy
  43. 0043intro hz
  44. 0044have hxstep : exists r. (exists ff_b_bie_mul_left_prefix ff_c_bie_mul_left_prefix. ((forall ff_i_bie_mul_left_prefix_repeat. (exists ff_lt_bie_mul_left_prefix_repeat_bound. ff_lt_bie_mul_left_prefix_repeat_bound + S ff_i_bie_mul_left_prefix_repeat = e) -> (((exists ff_h_bie_mul_left_prefix_repeat_decoded. ff_h_bie_mul_left_prefix_repeat_decoded + S (a) = S ((S (ff_i_bie_mul_left_prefix_repeat)) * ff_c_bie_mul_left_prefix)) /\ exists ff_q_bie_mul_left_prefix_repeat_decoded. ff_b_bie_mul_left_prefix = ff_q_bie_mul_left_prefix_repeat_decoded * S ((S (ff_i_bie_mul_left_prefix_repeat)) * ff_c_bie_mul_left_prefix) + (a)))) /\ (exists ff_u_bie_mul_left_prefix_product ff_v_bie_mul_left_prefix_product. ((((exists ff_h_bie_mul_left_prefix_product_start. ff_h_bie_mul_left_prefix_product_start + S (1) = S ((S (0)) * ff_v_bie_mul_left_prefix_product)) /\ exists ff_q_bie_mul_left_prefix_product_start. ff_u_bie_mul_left_prefix_product = ff_q_bie_mul_left_prefix_product_start * S ((S (0)) * ff_v_bie_mul_left_prefix_product) + (1))) /\ ((((exists ff_h_bie_mul_left_prefix_product_terminal. ff_h_bie_mul_left_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bie_mul_left_prefix_product)) /\ exists ff_q_bie_mul_left_prefix_product_terminal. ff_u_bie_mul_left_prefix_product = ff_q_bie_mul_left_prefix_product_terminal * S ((S (e)) * ff_v_bie_mul_left_prefix_product) + (r))) /\ forall ff_i_bie_mul_left_prefix_product. (exists ff_lt_bie_mul_left_prefix_product_bound. ff_lt_bie_mul_left_prefix_product_bound + S ff_i_bie_mul_left_prefix_product = e) -> exists ff_p_bie_mul_left_prefix_product ff_r_bie_mul_left_prefix_product ff_s_bie_mul_left_prefix_product. ((((exists ff_h_bie_mul_left_prefix_product_factor. ff_h_bie_mul_left_prefix_product_factor + S (ff_p_bie_mul_left_prefix_product) = S ((S (ff_i_bie_mul_left_prefix_product)) * ff_c_bie_mul_left_prefix)) /\ exists ff_q_bie_mul_left_prefix_product_factor. ff_b_bie_mul_left_prefix = ff_q_bie_mul_left_prefix_product_factor * S ((S (ff_i_bie_mul_left_prefix_product)) * ff_c_bie_mul_left_prefix) + (ff_p_bie_mul_left_prefix_product))) /\ ((((exists ff_h_bie_mul_left_prefix_product_partial. ff_h_bie_mul_left_prefix_product_partial + S (ff_r_bie_mul_left_prefix_product) = S ((S (ff_i_bie_mul_left_prefix_product)) * ff_v_bie_mul_left_prefix_product)) /\ exists ff_q_bie_mul_left_prefix_product_partial. ff_u_bie_mul_left_prefix_product = ff_q_bie_mul_left_prefix_product_partial * S ((S (ff_i_bie_mul_left_prefix_product)) * ff_v_bie_mul_left_prefix_product) + (ff_r_bie_mul_left_prefix_product))) /\ ((((exists ff_h_bie_mul_left_prefix_product_successor. ff_h_bie_mul_left_prefix_product_successor + S (ff_s_bie_mul_left_prefix_product) = S ((S (S ff_i_bie_mul_left_prefix_product)) * ff_v_bie_mul_left_prefix_product)) /\ exists ff_q_bie_mul_left_prefix_product_successor. ff_u_bie_mul_left_prefix_product = ff_q_bie_mul_left_prefix_product_successor * S ((S (S ff_i_bie_mul_left_prefix_product)) * ff_v_bie_mul_left_prefix_product) + (ff_s_bie_mul_left_prefix_product))) /\ ff_s_bie_mul_left_prefix_product = ff_r_bie_mul_left_prefix_product * ff_p_bie_mul_left_prefix_product)))))))) /\ x = r * a
  45. 0045specialize pow_successor_decompose a
  46. 0046specialize pow_successor_decompose e
  47. 0047specialize pow_successor_decompose (S e)
  48. 0048specialize pow_successor_decompose x
  49. 0049apply pow_successor_decompose
  50. 0050refl
  51. 0051exact hx
  52. 0052cases hxstep
  53. 0053cases hxstep_witness
  54. 0054have hystep : exists r. (exists ff_b_bie_mul_right_prefix ff_c_bie_mul_right_prefix. ((forall ff_i_bie_mul_right_prefix_repeat. (exists ff_lt_bie_mul_right_prefix_repeat_bound. ff_lt_bie_mul_right_prefix_repeat_bound + S ff_i_bie_mul_right_prefix_repeat = e) -> (((exists ff_h_bie_mul_right_prefix_repeat_decoded. ff_h_bie_mul_right_prefix_repeat_decoded + S (b) = S ((S (ff_i_bie_mul_right_prefix_repeat)) * ff_c_bie_mul_right_prefix)) /\ exists ff_q_bie_mul_right_prefix_repeat_decoded. ff_b_bie_mul_right_prefix = ff_q_bie_mul_right_prefix_repeat_decoded * S ((S (ff_i_bie_mul_right_prefix_repeat)) * ff_c_bie_mul_right_prefix) + (b)))) /\ (exists ff_u_bie_mul_right_prefix_product ff_v_bie_mul_right_prefix_product. ((((exists ff_h_bie_mul_right_prefix_product_start. ff_h_bie_mul_right_prefix_product_start + S (1) = S ((S (0)) * ff_v_bie_mul_right_prefix_product)) /\ exists ff_q_bie_mul_right_prefix_product_start. ff_u_bie_mul_right_prefix_product = ff_q_bie_mul_right_prefix_product_start * S ((S (0)) * ff_v_bie_mul_right_prefix_product) + (1))) /\ ((((exists ff_h_bie_mul_right_prefix_product_terminal. ff_h_bie_mul_right_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bie_mul_right_prefix_product)) /\ exists ff_q_bie_mul_right_prefix_product_terminal. ff_u_bie_mul_right_prefix_product = ff_q_bie_mul_right_prefix_product_terminal * S ((S (e)) * ff_v_bie_mul_right_prefix_product) + (r))) /\ forall ff_i_bie_mul_right_prefix_product. (exists ff_lt_bie_mul_right_prefix_product_bound. ff_lt_bie_mul_right_prefix_product_bound + S ff_i_bie_mul_right_prefix_product = e) -> exists ff_p_bie_mul_right_prefix_product ff_r_bie_mul_right_prefix_product ff_s_bie_mul_right_prefix_product. ((((exists ff_h_bie_mul_right_prefix_product_factor. ff_h_bie_mul_right_prefix_product_factor + S (ff_p_bie_mul_right_prefix_product) = S ((S (ff_i_bie_mul_right_prefix_product)) * ff_c_bie_mul_right_prefix)) /\ exists ff_q_bie_mul_right_prefix_product_factor. ff_b_bie_mul_right_prefix = ff_q_bie_mul_right_prefix_product_factor * S ((S (ff_i_bie_mul_right_prefix_product)) * ff_c_bie_mul_right_prefix) + (ff_p_bie_mul_right_prefix_product))) /\ ((((exists ff_h_bie_mul_right_prefix_product_partial. ff_h_bie_mul_right_prefix_product_partial + S (ff_r_bie_mul_right_prefix_product) = S ((S (ff_i_bie_mul_right_prefix_product)) * ff_v_bie_mul_right_prefix_product)) /\ exists ff_q_bie_mul_right_prefix_product_partial. ff_u_bie_mul_right_prefix_product = ff_q_bie_mul_right_prefix_product_partial * S ((S (ff_i_bie_mul_right_prefix_product)) * ff_v_bie_mul_right_prefix_product) + (ff_r_bie_mul_right_prefix_product))) /\ ((((exists ff_h_bie_mul_right_prefix_product_successor. ff_h_bie_mul_right_prefix_product_successor + S (ff_s_bie_mul_right_prefix_product) = S ((S (S ff_i_bie_mul_right_prefix_product)) * ff_v_bie_mul_right_prefix_product)) /\ exists ff_q_bie_mul_right_prefix_product_successor. ff_u_bie_mul_right_prefix_product = ff_q_bie_mul_right_prefix_product_successor * S ((S (S ff_i_bie_mul_right_prefix_product)) * ff_v_bie_mul_right_prefix_product) + (ff_s_bie_mul_right_prefix_product))) /\ ff_s_bie_mul_right_prefix_product = ff_r_bie_mul_right_prefix_product * ff_p_bie_mul_right_prefix_product)))))))) /\ y = r * b
  55. 0055specialize pow_successor_decompose b
  56. 0056specialize pow_successor_decompose e
  57. 0057specialize pow_successor_decompose (S e)
  58. 0058specialize pow_successor_decompose y
  59. 0059apply pow_successor_decompose
  60. 0060refl
  61. 0061exact hy
  62. 0062cases hystep
  63. 0063cases hystep_witness
  64. 0064have hzstep : exists r. (exists pa_b_bie_mul_product_prefix pa_c_bie_mul_product_prefix. ((forall pa_i_bie_mul_product_prefix_repeat. (exists pa_lt_bie_mul_product_prefix_repeat_bound. pa_lt_bie_mul_product_prefix_repeat_bound + S pa_i_bie_mul_product_prefix_repeat = e) -> (((exists pa_h_bie_mul_product_prefix_repeat_decoded. pa_h_bie_mul_product_prefix_repeat_decoded + S (a * b) = S ((S (pa_i_bie_mul_product_prefix_repeat)) * pa_c_bie_mul_product_prefix)) /\ exists pa_q_bie_mul_product_prefix_repeat_decoded. pa_b_bie_mul_product_prefix = pa_q_bie_mul_product_prefix_repeat_decoded * S ((S (pa_i_bie_mul_product_prefix_repeat)) * pa_c_bie_mul_product_prefix) + (a * b)))) /\ (exists pa_u_bie_mul_product_prefix_product pa_v_bie_mul_product_prefix_product. ((((exists pa_h_bie_mul_product_prefix_product_start. pa_h_bie_mul_product_prefix_product_start + S (1) = S ((S (0)) * pa_v_bie_mul_product_prefix_product)) /\ exists pa_q_bie_mul_product_prefix_product_start. pa_u_bie_mul_product_prefix_product = pa_q_bie_mul_product_prefix_product_start * S ((S (0)) * pa_v_bie_mul_product_prefix_product) + (1))) /\ ((((exists pa_h_bie_mul_product_prefix_product_terminal. pa_h_bie_mul_product_prefix_product_terminal + S (r) = S ((S (e)) * pa_v_bie_mul_product_prefix_product)) /\ exists pa_q_bie_mul_product_prefix_product_terminal. pa_u_bie_mul_product_prefix_product = pa_q_bie_mul_product_prefix_product_terminal * S ((S (e)) * pa_v_bie_mul_product_prefix_product) + (r))) /\ forall pa_i_bie_mul_product_prefix_product. (exists pa_lt_bie_mul_product_prefix_product_bound. pa_lt_bie_mul_product_prefix_product_bound + S pa_i_bie_mul_product_prefix_product = e) -> exists pa_p_bie_mul_product_prefix_product pa_r_bie_mul_product_prefix_product pa_s_bie_mul_product_prefix_product. ((((exists pa_h_bie_mul_product_prefix_product_factor. pa_h_bie_mul_product_prefix_product_factor + S (pa_p_bie_mul_product_prefix_product) = S ((S (pa_i_bie_mul_product_prefix_product)) * pa_c_bie_mul_product_prefix)) /\ exists pa_q_bie_mul_product_prefix_product_factor. pa_b_bie_mul_product_prefix = pa_q_bie_mul_product_prefix_product_factor * S ((S (pa_i_bie_mul_product_prefix_product)) * pa_c_bie_mul_product_prefix) + (pa_p_bie_mul_product_prefix_product))) /\ ((((exists pa_h_bie_mul_product_prefix_product_partial. pa_h_bie_mul_product_prefix_product_partial + S (pa_r_bie_mul_product_prefix_product) = S ((S (pa_i_bie_mul_product_prefix_product)) * pa_v_bie_mul_product_prefix_product)) /\ exists pa_q_bie_mul_product_prefix_product_partial. pa_u_bie_mul_product_prefix_product = pa_q_bie_mul_product_prefix_product_partial * S ((S (pa_i_bie_mul_product_prefix_product)) * pa_v_bie_mul_product_prefix_product) + (pa_r_bie_mul_product_prefix_product))) /\ ((((exists pa_h_bie_mul_product_prefix_product_successor. pa_h_bie_mul_product_prefix_product_successor + S (pa_s_bie_mul_product_prefix_product) = S ((S (S pa_i_bie_mul_product_prefix_product)) * pa_v_bie_mul_product_prefix_product)) /\ exists pa_q_bie_mul_product_prefix_product_successor. pa_u_bie_mul_product_prefix_product = pa_q_bie_mul_product_prefix_product_successor * S ((S (S pa_i_bie_mul_product_prefix_product)) * pa_v_bie_mul_product_prefix_product) + (pa_s_bie_mul_product_prefix_product))) /\ pa_s_bie_mul_product_prefix_product = pa_r_bie_mul_product_prefix_product * pa_p_bie_mul_product_prefix_product)))))))) /\ z = r * (a * b)
  65. 0065specialize pow_successor_decompose (a * b)
  66. 0066specialize pow_successor_decompose e
  67. 0067specialize pow_successor_decompose (S e)
  68. 0068specialize pow_successor_decompose z
  69. 0069apply pow_successor_decompose
  70. 0070refl
  71. 0071exact hz
  72. 0072cases hzstep
  73. 0073cases hzstep_witness
  74. 0074have hprefix : x3 = x1 * x2
  75. 0075specialize IH x1
  76. 0076specialize IH x2
  77. 0077specialize IH x3
  78. 0078apply IH
  79. 0079exact hxstep_witness_left
  80. 0080exact hystep_witness_left
  81. 0081exact hzstep_witness_left
  82. 0082trans x3 * (a * b)
  83. 0083exact hzstep_witness_right
  84. 0084trans (x1 * x2) * (a * b)
  85. 0085congr
  86. 0086exact hprefix
  87. 0087refl
  88. 0088trans x1 * (x2 * (a * b))
  89. 0089apply mul_assoc
  90. 0090trans x1 * ((x2 * a) * b)
  91. 0091congr
  92. 0092refl
  93. 0093symm
  94. 0094apply mul_assoc
  95. 0095trans x1 * ((a * x2) * b)
  96. 0096congr
  97. 0097refl
  98. 0098congr
  99. 0099apply mul_comm
  100. 0100refl
  101. 0101trans x1 * (a * (x2 * b))
  102. 0102congr
  103. 0103refl
  104. 0104apply mul_assoc
  105. 0105trans (x1 * a) * (x2 * b)
  106. 0106symm
  107. 0107apply mul_assoc
  108. 0108rewrite <- hxstep_witness_right
  109. 0109rewrite <- hystep_witness_right
  110. 0110refl