∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α] (x x_1 x_2 : Interval α),
  Option.map₂ (fun x1 x2 => x1 * x2) (Option.map₂ (fun x1 x2 => x1 * x2) x x_1) x_2 =
    Option.map₂ (fun x1 x2 => x1 * x2) x (Option.map₂ (fun x1 x2 => x1 * x2) x_1 x_2)