no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
⊢ (⨍ (x : ℝ) in Ι a b, f x) = ⨍ (x : ℝ) in Ι b a, f x
rw [set_average_eq, set_average_eq, uIoc_comm]