∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [MeasureTheory.IsFiniteMeasure μ] {p q : ENNReal}, p ≤ q → MeasureTheory.Lp E q μ ≤ MeasureTheory.Lp E p μ