DC0005

dirichlet_convolution_entry_quotient_product

A retained entry is the product at the specified actual quotient; nonzero multiplication cancellation identifies every quotient witness.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ n. ∀ d. ∀ q. ∀ a. ∀ b. ∀ z. ¬d = 0 → n = d · q → ArithAt(F,d,a) → ArithAt(G,q,b) → DirichletEntry(F,G,n,d,z) → SignedMul(a,b,z)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedMul(a,b,c) · 1ArithAt(F,i,z) · 2DirichletEntry(F,G,n,d,z) · 1

Actual proof prerequisites

mul_left_cancel_nonzero · checked external prerequisitedivisor_signed_table_at_functional · checked external prerequisite
Original expanded first-order statement 
forall F G n d q a b z. ~(d=0) -> n=d*q -> (exists dst_positive_code_read_left dst_positive_scale_read_left dst_negative_code_read_left dst_negative_scale_read_left dst_positive_read_left dst_negative_read_left. (((F) = (((((dst_positive_code_read_left) + (dst_positive_scale_read_left)) * S ((dst_positive_code_read_left) + (dst_positive_scale_read_left)) + ((dst_positive_scale_read_left) + (dst_positive_scale_read_left))) + (((dst_negative_code_read_left) + (dst_negative_scale_read_left)) * S ((dst_negative_code_read_left) + (dst_negative_scale_read_left)) + ((dst_negative_scale_read_left) + (dst_negative_scale_read_left)))) * S ((((dst_positive_code_read_left) + (dst_positive_scale_read_left)) * S ((dst_positive_code_read_left) + (dst_positive_scale_read_left)) + ((dst_positive_scale_read_left) + (dst_positive_scale_read_left))) + (((dst_negative_code_read_left) + (dst_negative_scale_read_left)) * S ((dst_negative_code_read_left) + (dst_negative_scale_read_left)) + ((dst_negative_scale_read_left) + (dst_negative_scale_read_left)))) + ((((dst_negative_code_read_left) + (dst_negative_scale_read_left)) * S ((dst_negative_code_read_left) + (dst_negative_scale_read_left)) + ((dst_negative_scale_read_left) + (dst_negative_scale_read_left))) + (((dst_negative_code_read_left) + (dst_negative_scale_read_left)) * S ((dst_negative_code_read_left) + (dst_negative_scale_read_left)) + ((dst_negative_scale_read_left) + (dst_negative_scale_read_left)))))) /\ (((((exists ff_h_pvs_read_leftpositive. ff_h_pvs_read_leftpositive + S (dst_positive_read_left) = S ((S (d)) * dst_positive_scale_read_left)) /\ exists ff_q_pvs_read_leftpositive. dst_positive_code_read_left = ff_q_pvs_read_leftpositive * S ((S (d)) * dst_positive_scale_read_left) + (dst_positive_read_left))) /\ (((((exists ff_h_pvs_read_leftnegative. ff_h_pvs_read_leftnegative + S (dst_negative_read_left) = S ((S (d)) * dst_negative_scale_read_left)) /\ exists ff_q_pvs_read_leftnegative. dst_negative_code_read_left = ff_q_pvs_read_leftnegative * S ((S (d)) * dst_negative_scale_read_left) + (dst_negative_read_left))) /\ (exists ge_balance_positive_read_leftvalue ge_balance_negative_read_leftvalue. (((((a) = 2 * (ge_balance_positive_read_leftvalue) /\ (ge_balance_negative_read_leftvalue) = 0) \/ exists ge_signed_half_read_leftvaluedecode. (((a) = 2 * ge_signed_half_read_leftvaluedecode + 1 /\ (ge_balance_positive_read_leftvalue) = 0) /\ (ge_balance_negative_read_leftvalue) = S ge_signed_half_read_leftvaluedecode))) /\ ((dst_positive_read_left) + ge_balance_negative_read_leftvalue = (dst_negative_read_left) + ge_balance_positive_read_leftvalue))))))))) -> (exists dst_positive_code_read_right dst_positive_scale_read_right dst_negative_code_read_right dst_negative_scale_read_right dst_positive_read_right dst_negative_read_right. (((G) = (((((dst_positive_code_read_right) + (dst_positive_scale_read_right)) * S ((dst_positive_code_read_right) + (dst_positive_scale_read_right)) + ((dst_positive_scale_read_right) + (dst_positive_scale_read_right))) + (((dst_negative_code_read_right) + (dst_negative_scale_read_right)) * S ((dst_negative_code_read_right) + (dst_negative_scale_read_right)) + ((dst_negative_scale_read_right) + (dst_negative_scale_read_right)))) * S ((((dst_positive_code_read_right) + (dst_positive_scale_read_right)) * S ((dst_positive_code_read_right) + (dst_positive_scale_read_right)) + ((dst_positive_scale_read_right) + (dst_positive_scale_read_right))) + (((dst_negative_code_read_right) + (dst_negative_scale_read_right)) * S ((dst_negative_code_read_right) + (dst_negative_scale_read_right)) + ((dst_negative_scale_read_right) + (dst_negative_scale_read_right)))) + ((((dst_negative_code_read_right) + (dst_negative_scale_read_right)) * S ((dst_negative_code_read_right) + (dst_negative_scale_read_right)) + ((dst_negative_scale_read_right) + (dst_negative_scale_read_right))) + (((dst_negative_code_read_right) + (dst_negative_scale_read_right)) * S ((dst_negative_code_read_right) + (dst_negative_scale_read_right)) + ((dst_negative_scale_read_right) + (dst_negative_scale_read_right)))))) /\ (((((exists ff_h_pvs_read_rightpositive. ff_h_pvs_read_rightpositive + S (dst_positive_read_right) = S ((S (q)) * dst_positive_scale_read_right)) /\ exists ff_q_pvs_read_rightpositive. dst_positive_code_read_right = ff_q_pvs_read_rightpositive * S ((S (q)) * dst_positive_scale_read_right) + (dst_positive_read_right))) /\ (((((exists ff_h_pvs_read_rightnegative. ff_h_pvs_read_rightnegative + S (dst_negative_read_right) = S ((S (q)) * dst_negative_scale_read_right)) /\ exists ff_q_pvs_read_rightnegative. dst_negative_code_read_right = ff_q_pvs_read_rightnegative * S ((S (q)) * dst_negative_scale_read_right) + (dst_negative_read_right))) /\ (exists ge_balance_positive_read_rightvalue ge_balance_negative_read_rightvalue. (((((b) = 2 * (ge_balance_positive_read_rightvalue) /\ (ge_balance_negative_read_rightvalue) = 0) \/ exists ge_signed_half_read_rightvaluedecode. (((b) = 2 * ge_signed_half_read_rightvaluedecode + 1 /\ (ge_balance_positive_read_rightvalue) = 0) /\ (ge_balance_negative_read_rightvalue) = S ge_signed_half_read_rightvaluedecode))) /\ ((dst_positive_read_right) + ge_balance_negative_read_rightvalue = (dst_negative_read_right) + ge_balance_positive_read_rightvalue))))))))) -> ((((~((d)=0)) /\ (exists dc_quotient_read_entry dc_left_read_entry dc_right_read_entry. (((n)=(d)*dc_quotient_read_entry) /\ (((exists dst_positive_code_read_entryleft dst_positive_scale_read_entryleft dst_negative_code_read_entryleft dst_negative_scale_read_entryleft dst_positive_read_entryleft dst_negative_read_entryleft. (((F) = (((((dst_positive_code_read_entryleft) + (dst_positive_scale_read_entryleft)) * S ((dst_positive_code_read_entryleft) + (dst_positive_scale_read_entryleft)) + ((dst_positive_scale_read_entryleft) + (dst_positive_scale_read_entryleft))) + (((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) * S ((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) + ((dst_negative_scale_read_entryleft) + (dst_negative_scale_read_entryleft)))) * S ((((dst_positive_code_read_entryleft) + (dst_positive_scale_read_entryleft)) * S ((dst_positive_code_read_entryleft) + (dst_positive_scale_read_entryleft)) + ((dst_positive_scale_read_entryleft) + (dst_positive_scale_read_entryleft))) + (((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) * S ((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) + ((dst_negative_scale_read_entryleft) + (dst_negative_scale_read_entryleft)))) + ((((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) * S ((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) + ((dst_negative_scale_read_entryleft) + (dst_negative_scale_read_entryleft))) + (((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) * S ((dst_negative_code_read_entryleft) + (dst_negative_scale_read_entryleft)) + ((dst_negative_scale_read_entryleft) + (dst_negative_scale_read_entryleft)))))) /\ (((((exists ff_h_pvs_read_entryleftpositive. ff_h_pvs_read_entryleftpositive + S (dst_positive_read_entryleft) = S ((S (d)) * dst_positive_scale_read_entryleft)) /\ exists ff_q_pvs_read_entryleftpositive. dst_positive_code_read_entryleft = ff_q_pvs_read_entryleftpositive * S ((S (d)) * dst_positive_scale_read_entryleft) + (dst_positive_read_entryleft))) /\ (((((exists ff_h_pvs_read_entryleftnegative. ff_h_pvs_read_entryleftnegative + S (dst_negative_read_entryleft) = S ((S (d)) * dst_negative_scale_read_entryleft)) /\ exists ff_q_pvs_read_entryleftnegative. dst_negative_code_read_entryleft = ff_q_pvs_read_entryleftnegative * S ((S (d)) * dst_negative_scale_read_entryleft) + (dst_negative_read_entryleft))) /\ (exists ge_balance_positive_read_entryleftvalue ge_balance_negative_read_entryleftvalue. (((((dc_left_read_entry) = 2 * (ge_balance_positive_read_entryleftvalue) /\ (ge_balance_negative_read_entryleftvalue) = 0) \/ exists ge_signed_half_read_entryleftvaluedecode. (((dc_left_read_entry) = 2 * ge_signed_half_read_entryleftvaluedecode + 1 /\ (ge_balance_positive_read_entryleftvalue) = 0) /\ (ge_balance_negative_read_entryleftvalue) = S ge_signed_half_read_entryleftvaluedecode))) /\ ((dst_positive_read_entryleft) + ge_balance_negative_read_entryleftvalue = (dst_negative_read_entryleft) + ge_balance_positive_read_entryleftvalue))))))))) /\ (((exists dst_positive_code_read_entryright dst_positive_scale_read_entryright dst_negative_code_read_entryright dst_negative_scale_read_entryright dst_positive_read_entryright dst_negative_read_entryright. (((G) = (((((dst_positive_code_read_entryright) + (dst_positive_scale_read_entryright)) * S ((dst_positive_code_read_entryright) + (dst_positive_scale_read_entryright)) + ((dst_positive_scale_read_entryright) + (dst_positive_scale_read_entryright))) + (((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) * S ((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) + ((dst_negative_scale_read_entryright) + (dst_negative_scale_read_entryright)))) * S ((((dst_positive_code_read_entryright) + (dst_positive_scale_read_entryright)) * S ((dst_positive_code_read_entryright) + (dst_positive_scale_read_entryright)) + ((dst_positive_scale_read_entryright) + (dst_positive_scale_read_entryright))) + (((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) * S ((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) + ((dst_negative_scale_read_entryright) + (dst_negative_scale_read_entryright)))) + ((((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) * S ((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) + ((dst_negative_scale_read_entryright) + (dst_negative_scale_read_entryright))) + (((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) * S ((dst_negative_code_read_entryright) + (dst_negative_scale_read_entryright)) + ((dst_negative_scale_read_entryright) + (dst_negative_scale_read_entryright)))))) /\ (((((exists ff_h_pvs_read_entryrightpositive. ff_h_pvs_read_entryrightpositive + S (dst_positive_read_entryright) = S ((S (dc_quotient_read_entry)) * dst_positive_scale_read_entryright)) /\ exists ff_q_pvs_read_entryrightpositive. dst_positive_code_read_entryright = ff_q_pvs_read_entryrightpositive * S ((S (dc_quotient_read_entry)) * dst_positive_scale_read_entryright) + (dst_positive_read_entryright))) /\ (((((exists ff_h_pvs_read_entryrightnegative. ff_h_pvs_read_entryrightnegative + S (dst_negative_read_entryright) = S ((S (dc_quotient_read_entry)) * dst_negative_scale_read_entryright)) /\ exists ff_q_pvs_read_entryrightnegative. dst_negative_code_read_entryright = ff_q_pvs_read_entryrightnegative * S ((S (dc_quotient_read_entry)) * dst_negative_scale_read_entryright) + (dst_negative_read_entryright))) /\ (exists ge_balance_positive_read_entryrightvalue ge_balance_negative_read_entryrightvalue. (((((dc_right_read_entry) = 2 * (ge_balance_positive_read_entryrightvalue) /\ (ge_balance_negative_read_entryrightvalue) = 0) \/ exists ge_signed_half_read_entryrightvaluedecode. (((dc_right_read_entry) = 2 * ge_signed_half_read_entryrightvaluedecode + 1 /\ (ge_balance_positive_read_entryrightvalue) = 0) /\ (ge_balance_negative_read_entryrightvalue) = S ge_signed_half_read_entryrightvaluedecode))) /\ ((dst_positive_read_entryright) + ge_balance_negative_read_entryrightvalue = (dst_negative_read_entryright) + ge_balance_positive_read_entryrightvalue))))))))) /\ (exists sto_ap_read_entryproduct sto_an_read_entryproduct sto_bp_read_entryproduct sto_bn_read_entryproduct sto_cp_read_entryproduct sto_cn_read_entryproduct. (((((dc_left_read_entry) = 2 * (sto_ap_read_entryproduct) /\ (sto_an_read_entryproduct) = 0) \/ exists ge_signed_half_read_entryproductleft. (((dc_left_read_entry) = 2 * ge_signed_half_read_entryproductleft + 1 /\ (sto_ap_read_entryproduct) = 0) /\ (sto_an_read_entryproduct) = S ge_signed_half_read_entryproductleft))) /\ ((((((dc_right_read_entry) = 2 * (sto_bp_read_entryproduct) /\ (sto_bn_read_entryproduct) = 0) \/ exists ge_signed_half_read_entryproductright. (((dc_right_read_entry) = 2 * ge_signed_half_read_entryproductright + 1 /\ (sto_bp_read_entryproduct) = 0) /\ (sto_bn_read_entryproduct) = S ge_signed_half_read_entryproductright))) /\ ((((((z) = 2 * (sto_cp_read_entryproduct) /\ (sto_cn_read_entryproduct) = 0) \/ exists ge_signed_half_read_entryproductoutput. (((z) = 2 * ge_signed_half_read_entryproductoutput + 1 /\ (sto_cp_read_entryproduct) = 0) /\ (sto_cn_read_entryproduct) = S ge_signed_half_read_entryproductoutput))) /\ ((sto_ap_read_entryproduct * sto_bp_read_entryproduct + sto_an_read_entryproduct * sto_bn_read_entryproduct) + sto_cn_read_entryproduct = (sto_ap_read_entryproduct * sto_bn_read_entryproduct + sto_an_read_entryproduct * sto_bp_read_entryproduct) + sto_cp_read_entryproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_read_entrynondivisor. (n) = (d) * pvs_factor_read_entrynondivisor)) /\ ((z)=0)))) -> (exists sto_ap_read_product sto_an_read_product sto_bp_read_product sto_bn_read_product sto_cp_read_product sto_cn_read_product. (((((a) = 2 * (sto_ap_read_product) /\ (sto_an_read_product) = 0) \/ exists ge_signed_half_read_productleft. (((a) = 2 * ge_signed_half_read_productleft + 1 /\ (sto_ap_read_product) = 0) /\ (sto_an_read_product) = S ge_signed_half_read_productleft))) /\ ((((((b) = 2 * (sto_bp_read_product) /\ (sto_bn_read_product) = 0) \/ exists ge_signed_half_read_productright. (((b) = 2 * ge_signed_half_read_productright + 1 /\ (sto_bp_read_product) = 0) /\ (sto_bn_read_product) = S ge_signed_half_read_productright))) /\ ((((((z) = 2 * (sto_cp_read_product) /\ (sto_cn_read_product) = 0) \/ exists ge_signed_half_read_productoutput. (((z) = 2 * ge_signed_half_read_productoutput + 1 /\ (sto_cp_read_product) = 0) /\ (sto_cn_read_product) = S ge_signed_half_read_productoutput))) /\ ((sto_ap_read_product * sto_bp_read_product + sto_an_read_product * sto_bn_read_product) + sto_cn_read_product = (sto_ap_read_product * sto_bn_read_product + sto_an_read_product * sto_bp_read_product) + sto_cp_read_product)))))))

Complete tactic proof in conservative notation

All 64 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

64 script commands · 13 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro n
  4. L4
    intro d
  5. L5
    intro q
  6. L6
    intro a
  7. L7
    intro b
  8. L8
    intro z
  9. L9
    intro hd
  10. L10
    intro hq
02Fix variables and assumptionsL11–13

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro ha
  2. L12
    intro hb
  3. L13
    intro he
03Separate the logical casesL14–21

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases he
  2. L15
    cases he_left
  3. L16
    cases he_left_right
  4. L17
    cases he_left_right_witness
  5. L18
    cases he_left_right_witness_witness
  6. L19
    cases he_left_right_witness_witness_witness
  7. L20
    cases he_left_right_witness_witness_witness_right
  8. L21
    cases he_left_right_witness_witness_witness_right_right
04Establish heqqL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul left cancel nonzero.

  1. L22
    have heqq : x=q
  2. L23
    specialize mul_left_cancel_nonzero (d)
  3. L24
    specialize mul_left_cancel_nonzero (x)
  4. L25
    specialize mul_left_cancel_nonzero (q)
  5. L26
    apply mul_left_cancel_nonzero
  6. L27
    exact hd
  7. L28
    trans n
  8. L29
    symm
  9. L30
    exact he_left_right_witness_witness_witness_left
  10. L31
    exact hq
05Calculate and transport equalitiesL32–35

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    rewrite heqq at he_left_right_witness_witness_witness_right_right_left
  2. L33
    rewrite heqq at he_left_right_witness_witness_witness_right_right_left
  3. L34
    rewrite heqq at he_left_right_witness_witness_witness_right_right_left
  4. L35
    rewrite heqq at he_left_right_witness_witness_witness_right_right_left
06Establish heqaL36–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at functional.

  1. L36
    have heqa : x1=a
  2. L37
    specialize divisor_signed_table_at_functional (F)
  3. L38
    specialize divisor_signed_table_at_functional (d)
  4. L39
    specialize divisor_signed_table_at_functional (x1)
  5. L40
    specialize divisor_signed_table_at_functional (a)
  6. L41
    apply divisor_signed_table_at_functional
  7. L42
    exact he_left_right_witness_witness_witness_right_left
  8. L43
    exact ha
07Establish heqbL44–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at functional.

  1. L44
    have heqb : x2=b
  2. L45
    specialize divisor_signed_table_at_functional (G)
  3. L46
    specialize divisor_signed_table_at_functional (q)
  4. L47
    specialize divisor_signed_table_at_functional (x2)
  5. L48
    specialize divisor_signed_table_at_functional (b)
  6. L49
    apply divisor_signed_table_at_functional
  7. L50
    exact he_left_right_witness_witness_witness_right_right_left
  8. L51
    exact hb
  9. L52
    rewrite heqa at he_left_right_witness_witness_witness_right_right_right
  10. L53
    rewrite heqa at he_left_right_witness_witness_witness_right_right_right
08Calculate and transport equalitiesL54–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L54
    rewrite heqb at he_left_right_witness_witness_witness_right_right_right
  2. L55
    rewrite heqb at he_left_right_witness_witness_witness_right_right_right
09Use earlier factsL56–56

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L56
    exact he_left_right_witness_witness_witness_right_right_right
10Separate the logical casesL57–59

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L57
    cases he_right
  2. L58
    exfalso
  3. L59
    cases he_right_left
11Use earlier factsL60–62

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L60
    apply hd
  2. L61
    exact he_right_left_left
  3. L62
    apply he_right_left_right
12Construct an explicit witnessL63–63

Supply the displayed value, then prove that it has the required property.

  1. L63
    exists q
13Use earlier factsL64–64

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L64
    exact hq

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro d
  5. 0005intro q
  6. 0006intro a
  7. 0007intro b
  8. 0008intro z
  9. 0009intro hd
  10. 0010intro hq
  11. 0011intro ha
  12. 0012intro hb
  13. 0013intro he
  14. 0014cases he
  15. 0015cases he_left
  16. 0016cases he_left_right
  17. 0017cases he_left_right_witness
  18. 0018cases he_left_right_witness_witness
  19. 0019cases he_left_right_witness_witness_witness
  20. 0020cases he_left_right_witness_witness_witness_right
  21. 0021cases he_left_right_witness_witness_witness_right_right
  22. 0022have heqq : x=q
  23. 0023specialize mul_left_cancel_nonzero (d)
  24. 0024specialize mul_left_cancel_nonzero (x)
  25. 0025specialize mul_left_cancel_nonzero (q)
  26. 0026apply mul_left_cancel_nonzero
  27. 0027exact hd
  28. 0028trans n
  29. 0029symm
  30. 0030exact he_left_right_witness_witness_witness_left
  31. 0031exact hq
  32. 0032rewrite heqq at he_left_right_witness_witness_witness_right_right_left
  33. 0033rewrite heqq at he_left_right_witness_witness_witness_right_right_left
  34. 0034rewrite heqq at he_left_right_witness_witness_witness_right_right_left
  35. 0035rewrite heqq at he_left_right_witness_witness_witness_right_right_left
  36. 0036have heqa : x1=a
  37. 0037specialize divisor_signed_table_at_functional (F)
  38. 0038specialize divisor_signed_table_at_functional (d)
  39. 0039specialize divisor_signed_table_at_functional (x1)
  40. 0040specialize divisor_signed_table_at_functional (a)
  41. 0041apply divisor_signed_table_at_functional
  42. 0042exact he_left_right_witness_witness_witness_right_left
  43. 0043exact ha
  44. 0044have heqb : x2=b
  45. 0045specialize divisor_signed_table_at_functional (G)
  46. 0046specialize divisor_signed_table_at_functional (q)
  47. 0047specialize divisor_signed_table_at_functional (x2)
  48. 0048specialize divisor_signed_table_at_functional (b)
  49. 0049apply divisor_signed_table_at_functional
  50. 0050exact he_left_right_witness_witness_witness_right_right_left
  51. 0051exact hb
  52. 0052rewrite heqa at he_left_right_witness_witness_witness_right_right_right
  53. 0053rewrite heqa at he_left_right_witness_witness_witness_right_right_right
  54. 0054rewrite heqb at he_left_right_witness_witness_witness_right_right_right
  55. 0055rewrite heqb at he_left_right_witness_witness_witness_right_right_right
  56. 0056exact he_left_right_witness_witness_witness_right_right_right
  57. 0057cases he_right
  58. 0058exfalso
  59. 0059cases he_right_left
  60. 0060apply hd
  61. 0061exact he_right_left_left
  62. 0062apply he_right_left_right
  63. 0063exists q
  64. 0064exact hq