have : ∀ x ∈ Icc a b, ¬x ≤ b := by
  intro x hx hn
  apply hab
  rw [mem_Icc] at hx
  exact le_trans hx.1 hn
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (IncidenceAlgebra.mu' 𝕜) a b = -∑ x ∈ Ioc a b, (IncidenceAlgebra.mu' 𝕜) x b
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 0
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this✝ : (IncidenceAlgebra.mu' 𝕜) a b = -∑ x ∈ Ioc a b, (IncidenceAlgebra.mu' 𝕜) x b
hab : ¬a ≤ b
this : ∀ x ∈ Icc a b, ¬x ≤ b
⊢ ∑ x ∈ Icc a b, (IncidenceAlgebra.mu' 𝕜) x b = 0