∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α],
  Interval.commMonoid =
    { toMul := Interval.mulOneClass.toMul, mul_assoc := ⋯, toOne := Interval.mulOneClass.toOne, one_mul := ⋯,
      mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }