∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a₁ a₂ b : α), toIcoMod hp a₁ (toIcoMod hp a₂ b) = toIcoMod hp a₁ b