∀ {𝕜 : Type u_1} {𝕝 : Type u_3} {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Semiring 𝕜]
  [inst_3 : Semiring 𝕝] [inst_4 : Module 𝕜 𝕝] (x y : IncidenceAlgebra 𝕜 α) (z : IncidenceAlgebra 𝕝 α),
  (x • y) • z = x • y • z