IV0003

dirichlet_kronecker_delta_table_restrict

The same actual delta table restricts to every smaller positive window, without changing its unrelated zeroth value.

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.

For an actual table an inverse exists exactly when N=0 or F(1) is signed +1 or -1. At a positive window this is the unit-at-one criterion; the empty window imposes no condition at one. Every inverse has actual delta and two-sided convolution witnesses. Its zeroth value is arbitrary, so uniqueness is positive-value equality, not equality of codes or of zeroth values. Multiplicative-function closure and full finite signed G009 are admitted in the separate Alpha-v32 multiplicative-convolution family.

Exact theorem in conservative defined notation

∀ N. ∀ K. ∀ E. KroneckerDeltaTable(N,E) → Le(K,N) → KroneckerDeltaTable(K,E)

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

Definition DAG

KroneckerDeltaTable(N,E) · 2Le(a,b) · 1

Actual proof prerequisites

divisor_signed_table_restrict · checked external prerequisitele_trans · checked external prerequisite
Original expanded first-order statement 
forall N K E. (((exists dst_positive_code_delta_restrict_sourcetable dst_positive_scale_delta_restrict_sourcetable dst_negative_code_delta_restrict_sourcetable dst_negative_scale_delta_restrict_sourcetable. (((E) = (((((dst_positive_code_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable)) * S ((dst_positive_code_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable)) + ((dst_positive_scale_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable))) + (((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) * S ((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) + ((dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)))) * S ((((dst_positive_code_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable)) * S ((dst_positive_code_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable)) + ((dst_positive_scale_delta_restrict_sourcetable) + (dst_positive_scale_delta_restrict_sourcetable))) + (((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) * S ((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) + ((dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)))) + ((((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) * S ((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) + ((dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable))) + (((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) * S ((dst_negative_code_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)) + ((dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_scale_delta_restrict_sourcetable)))))) /\ (forall dst_index_delta_restrict_sourcetable. (exists pvs_le_gap_delta_restrict_sourcetabledomain. pvs_le_gap_delta_restrict_sourcetabledomain + (dst_index_delta_restrict_sourcetable) = (N)) -> exists dst_positive_delta_restrict_sourcetable dst_negative_delta_restrict_sourcetable dst_value_delta_restrict_sourcetable. ((((exists ff_h_pvs_delta_restrict_sourcetableentrypositive. ff_h_pvs_delta_restrict_sourcetableentrypositive + S (dst_positive_delta_restrict_sourcetable) = S ((S (dst_index_delta_restrict_sourcetable)) * dst_positive_scale_delta_restrict_sourcetable)) /\ exists ff_q_pvs_delta_restrict_sourcetableentrypositive. dst_positive_code_delta_restrict_sourcetable = ff_q_pvs_delta_restrict_sourcetableentrypositive * S ((S (dst_index_delta_restrict_sourcetable)) * dst_positive_scale_delta_restrict_sourcetable) + (dst_positive_delta_restrict_sourcetable))) /\ (((((exists ff_h_pvs_delta_restrict_sourcetableentrynegative. ff_h_pvs_delta_restrict_sourcetableentrynegative + S (dst_negative_delta_restrict_sourcetable) = S ((S (dst_index_delta_restrict_sourcetable)) * dst_negative_scale_delta_restrict_sourcetable)) /\ exists ff_q_pvs_delta_restrict_sourcetableentrynegative. dst_negative_code_delta_restrict_sourcetable = ff_q_pvs_delta_restrict_sourcetableentrynegative * S ((S (dst_index_delta_restrict_sourcetable)) * dst_negative_scale_delta_restrict_sourcetable) + (dst_negative_delta_restrict_sourcetable))) /\ (exists ge_balance_positive_delta_restrict_sourcetableentryvalue ge_balance_negative_delta_restrict_sourcetableentryvalue. (((((dst_value_delta_restrict_sourcetable) = 2 * (ge_balance_positive_delta_restrict_sourcetableentryvalue) /\ (ge_balance_negative_delta_restrict_sourcetableentryvalue) = 0) \/ exists ge_signed_half_delta_restrict_sourcetableentryvaluedecode. (((dst_value_delta_restrict_sourcetable) = 2 * ge_signed_half_delta_restrict_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_delta_restrict_sourcetableentryvalue) = 0) /\ (ge_balance_negative_delta_restrict_sourcetableentryvalue) = S ge_signed_half_delta_restrict_sourcetableentryvaluedecode))) /\ ((dst_positive_delta_restrict_sourcetable) + ge_balance_negative_delta_restrict_sourcetableentryvalue = (dst_negative_delta_restrict_sourcetable) + ge_balance_positive_delta_restrict_sourcetableentryvalue))))))))) /\ (forall du_index_delta_restrict_source du_value_delta_restrict_source. ~(du_index_delta_restrict_source=0) -> (exists pvs_le_gap_delta_restrict_sourcebound. pvs_le_gap_delta_restrict_sourcebound + (du_index_delta_restrict_source) = (N)) -> (exists dst_positive_code_delta_restrict_sourceentry dst_positive_scale_delta_restrict_sourceentry dst_negative_code_delta_restrict_sourceentry dst_negative_scale_delta_restrict_sourceentry dst_positive_delta_restrict_sourceentry dst_negative_delta_restrict_sourceentry. (((E) = (((((dst_positive_code_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry)) * S ((dst_positive_code_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry)) + ((dst_positive_scale_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry))) + (((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) * S ((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) + ((dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)))) * S ((((dst_positive_code_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry)) * S ((dst_positive_code_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry)) + ((dst_positive_scale_delta_restrict_sourceentry) + (dst_positive_scale_delta_restrict_sourceentry))) + (((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) * S ((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) + ((dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)))) + ((((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) * S ((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) + ((dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry))) + (((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) * S ((dst_negative_code_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)) + ((dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_scale_delta_restrict_sourceentry)))))) /\ (((((exists ff_h_pvs_delta_restrict_sourceentrypositive. ff_h_pvs_delta_restrict_sourceentrypositive + S (dst_positive_delta_restrict_sourceentry) = S ((S (du_index_delta_restrict_source)) * dst_positive_scale_delta_restrict_sourceentry)) /\ exists ff_q_pvs_delta_restrict_sourceentrypositive. dst_positive_code_delta_restrict_sourceentry = ff_q_pvs_delta_restrict_sourceentrypositive * S ((S (du_index_delta_restrict_source)) * dst_positive_scale_delta_restrict_sourceentry) + (dst_positive_delta_restrict_sourceentry))) /\ (((((exists ff_h_pvs_delta_restrict_sourceentrynegative. ff_h_pvs_delta_restrict_sourceentrynegative + S (dst_negative_delta_restrict_sourceentry) = S ((S (du_index_delta_restrict_source)) * dst_negative_scale_delta_restrict_sourceentry)) /\ exists ff_q_pvs_delta_restrict_sourceentrynegative. dst_negative_code_delta_restrict_sourceentry = ff_q_pvs_delta_restrict_sourceentrynegative * S ((S (du_index_delta_restrict_source)) * dst_negative_scale_delta_restrict_sourceentry) + (dst_negative_delta_restrict_sourceentry))) /\ (exists ge_balance_positive_delta_restrict_sourceentryvalue ge_balance_negative_delta_restrict_sourceentryvalue. (((((du_value_delta_restrict_source) = 2 * (ge_balance_positive_delta_restrict_sourceentryvalue) /\ (ge_balance_negative_delta_restrict_sourceentryvalue) = 0) \/ exists ge_signed_half_delta_restrict_sourceentryvaluedecode. (((du_value_delta_restrict_source) = 2 * ge_signed_half_delta_restrict_sourceentryvaluedecode + 1 /\ (ge_balance_positive_delta_restrict_sourceentryvalue) = 0) /\ (ge_balance_negative_delta_restrict_sourceentryvalue) = S ge_signed_half_delta_restrict_sourceentryvaluedecode))) /\ ((dst_positive_delta_restrict_sourceentry) + ge_balance_negative_delta_restrict_sourceentryvalue = (dst_negative_delta_restrict_sourceentry) + ge_balance_positive_delta_restrict_sourceentryvalue))))))))) -> ((((du_index_delta_restrict_source)=1 -> (du_value_delta_restrict_source)=2) /\ (~((du_index_delta_restrict_source)=1) -> (du_value_delta_restrict_source)=0)))))) -> (exists pvs_le_gap_delta_restrict_bound. pvs_le_gap_delta_restrict_bound + (K) = (N)) -> (((exists dst_positive_code_delta_restrict_resulttable dst_positive_scale_delta_restrict_resulttable dst_negative_code_delta_restrict_resulttable dst_negative_scale_delta_restrict_resulttable. (((E) = (((((dst_positive_code_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable)) * S ((dst_positive_code_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable)) + ((dst_positive_scale_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable))) + (((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) * S ((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) + ((dst_negative_scale_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)))) * S ((((dst_positive_code_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable)) * S ((dst_positive_code_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable)) + ((dst_positive_scale_delta_restrict_resulttable) + (dst_positive_scale_delta_restrict_resulttable))) + (((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) * S ((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) + ((dst_negative_scale_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)))) + ((((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) * S ((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) + ((dst_negative_scale_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable))) + (((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) * S ((dst_negative_code_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)) + ((dst_negative_scale_delta_restrict_resulttable) + (dst_negative_scale_delta_restrict_resulttable)))))) /\ (forall dst_index_delta_restrict_resulttable. (exists pvs_le_gap_delta_restrict_resulttabledomain. pvs_le_gap_delta_restrict_resulttabledomain + (dst_index_delta_restrict_resulttable) = (K)) -> exists dst_positive_delta_restrict_resulttable dst_negative_delta_restrict_resulttable dst_value_delta_restrict_resulttable. ((((exists ff_h_pvs_delta_restrict_resulttableentrypositive. ff_h_pvs_delta_restrict_resulttableentrypositive + S (dst_positive_delta_restrict_resulttable) = S ((S (dst_index_delta_restrict_resulttable)) * dst_positive_scale_delta_restrict_resulttable)) /\ exists ff_q_pvs_delta_restrict_resulttableentrypositive. dst_positive_code_delta_restrict_resulttable = ff_q_pvs_delta_restrict_resulttableentrypositive * S ((S (dst_index_delta_restrict_resulttable)) * dst_positive_scale_delta_restrict_resulttable) + (dst_positive_delta_restrict_resulttable))) /\ (((((exists ff_h_pvs_delta_restrict_resulttableentrynegative. ff_h_pvs_delta_restrict_resulttableentrynegative + S (dst_negative_delta_restrict_resulttable) = S ((S (dst_index_delta_restrict_resulttable)) * dst_negative_scale_delta_restrict_resulttable)) /\ exists ff_q_pvs_delta_restrict_resulttableentrynegative. dst_negative_code_delta_restrict_resulttable = ff_q_pvs_delta_restrict_resulttableentrynegative * S ((S (dst_index_delta_restrict_resulttable)) * dst_negative_scale_delta_restrict_resulttable) + (dst_negative_delta_restrict_resulttable))) /\ (exists ge_balance_positive_delta_restrict_resulttableentryvalue ge_balance_negative_delta_restrict_resulttableentryvalue. (((((dst_value_delta_restrict_resulttable) = 2 * (ge_balance_positive_delta_restrict_resulttableentryvalue) /\ (ge_balance_negative_delta_restrict_resulttableentryvalue) = 0) \/ exists ge_signed_half_delta_restrict_resulttableentryvaluedecode. (((dst_value_delta_restrict_resulttable) = 2 * ge_signed_half_delta_restrict_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_delta_restrict_resulttableentryvalue) = 0) /\ (ge_balance_negative_delta_restrict_resulttableentryvalue) = S ge_signed_half_delta_restrict_resulttableentryvaluedecode))) /\ ((dst_positive_delta_restrict_resulttable) + ge_balance_negative_delta_restrict_resulttableentryvalue = (dst_negative_delta_restrict_resulttable) + ge_balance_positive_delta_restrict_resulttableentryvalue))))))))) /\ (forall du_index_delta_restrict_result du_value_delta_restrict_result. ~(du_index_delta_restrict_result=0) -> (exists pvs_le_gap_delta_restrict_resultbound. pvs_le_gap_delta_restrict_resultbound + (du_index_delta_restrict_result) = (K)) -> (exists dst_positive_code_delta_restrict_resultentry dst_positive_scale_delta_restrict_resultentry dst_negative_code_delta_restrict_resultentry dst_negative_scale_delta_restrict_resultentry dst_positive_delta_restrict_resultentry dst_negative_delta_restrict_resultentry. (((E) = (((((dst_positive_code_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry)) * S ((dst_positive_code_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry)) + ((dst_positive_scale_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry))) + (((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) * S ((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) + ((dst_negative_scale_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)))) * S ((((dst_positive_code_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry)) * S ((dst_positive_code_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry)) + ((dst_positive_scale_delta_restrict_resultentry) + (dst_positive_scale_delta_restrict_resultentry))) + (((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) * S ((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) + ((dst_negative_scale_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)))) + ((((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) * S ((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) + ((dst_negative_scale_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry))) + (((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) * S ((dst_negative_code_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)) + ((dst_negative_scale_delta_restrict_resultentry) + (dst_negative_scale_delta_restrict_resultentry)))))) /\ (((((exists ff_h_pvs_delta_restrict_resultentrypositive. ff_h_pvs_delta_restrict_resultentrypositive + S (dst_positive_delta_restrict_resultentry) = S ((S (du_index_delta_restrict_result)) * dst_positive_scale_delta_restrict_resultentry)) /\ exists ff_q_pvs_delta_restrict_resultentrypositive. dst_positive_code_delta_restrict_resultentry = ff_q_pvs_delta_restrict_resultentrypositive * S ((S (du_index_delta_restrict_result)) * dst_positive_scale_delta_restrict_resultentry) + (dst_positive_delta_restrict_resultentry))) /\ (((((exists ff_h_pvs_delta_restrict_resultentrynegative. ff_h_pvs_delta_restrict_resultentrynegative + S (dst_negative_delta_restrict_resultentry) = S ((S (du_index_delta_restrict_result)) * dst_negative_scale_delta_restrict_resultentry)) /\ exists ff_q_pvs_delta_restrict_resultentrynegative. dst_negative_code_delta_restrict_resultentry = ff_q_pvs_delta_restrict_resultentrynegative * S ((S (du_index_delta_restrict_result)) * dst_negative_scale_delta_restrict_resultentry) + (dst_negative_delta_restrict_resultentry))) /\ (exists ge_balance_positive_delta_restrict_resultentryvalue ge_balance_negative_delta_restrict_resultentryvalue. (((((du_value_delta_restrict_result) = 2 * (ge_balance_positive_delta_restrict_resultentryvalue) /\ (ge_balance_negative_delta_restrict_resultentryvalue) = 0) \/ exists ge_signed_half_delta_restrict_resultentryvaluedecode. (((du_value_delta_restrict_result) = 2 * ge_signed_half_delta_restrict_resultentryvaluedecode + 1 /\ (ge_balance_positive_delta_restrict_resultentryvalue) = 0) /\ (ge_balance_negative_delta_restrict_resultentryvalue) = S ge_signed_half_delta_restrict_resultentryvaluedecode))) /\ ((dst_positive_delta_restrict_resultentry) + ge_balance_negative_delta_restrict_resultentryvalue = (dst_negative_delta_restrict_resultentry) + ge_balance_positive_delta_restrict_resultentryvalue))))))))) -> ((((du_index_delta_restrict_result)=1 -> (du_value_delta_restrict_result)=2) /\ (~((du_index_delta_restrict_result)=1) -> (du_value_delta_restrict_result)=0))))))

Complete tactic proof in conservative notation

All 29 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

29 script commands · 6 reading checkpoints · 0 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–5

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

  1. L1
    intro N
  2. L2
    intro K
  3. L3
    intro E
  4. L4
    intro hd
  5. L5
    intro hK
02Separate the logical casesL6–7

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

  1. L6
    cases hd
  2. L7
    split
03Use earlier factsL8–13

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

  1. L8
    specialize divisor_signed_table_restrict (N)
  2. L9
    specialize divisor_signed_table_restrict (K)
  3. L10
    specialize divisor_signed_table_restrict (E)
  4. L11
    apply divisor_signed_table_restrict
  5. L12
    exact hd_left
  6. L13
    exact hK
04Fix variables and assumptionsL14–18

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

  1. L14
    intro n
  2. L15
    intro z
  3. L16
    intro hn
  4. L17
    intro hb
  5. L18
    intro hz
05Use earlier factsL19–28

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

  1. L19
    specialize hd_right (n)
  2. L20
    specialize hd_right (z)
  3. L21
    apply hd_right
  4. L22
    exact hn
  5. L23
    specialize le_trans (n)
  6. L24
    specialize le_trans (K)
  7. L25
    specialize le_trans (N)
  8. L26
    apply le_trans
  9. L27
    exact hb
  10. L28
    exact hK
06Use earlier factsL29–29

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

  1. L29
    exact hz

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro N
  2. 0002intro K
  3. 0003intro E
  4. 0004intro hd
  5. 0005intro hK
  6. 0006cases hd
  7. 0007split
  8. 0008specialize divisor_signed_table_restrict (N)
  9. 0009specialize divisor_signed_table_restrict (K)
  10. 0010specialize divisor_signed_table_restrict (E)
  11. 0011apply divisor_signed_table_restrict
  12. 0012exact hd_left
  13. 0013exact hK
  14. 0014intro n
  15. 0015intro z
  16. 0016intro hn
  17. 0017intro hb
  18. 0018intro hz
  19. 0019specialize hd_right (n)
  20. 0020specialize hd_right (z)
  21. 0021apply hd_right
  22. 0022exact hn
  23. 0023specialize le_trans (n)
  24. 0024specialize le_trans (K)
  25. 0025specialize le_trans (N)
  26. 0026apply le_trans
  27. 0027exact hb
  28. 0028exact hK
  29. 0029exact hz