Theory Utils

theory Utils
  imports 
    HOL.Real 
begin

lemma difference_in_sum' :
  fixes f:: "'a ⇒ real"
  fixes g:: "'a ⇒ real"
  assumes A:" (∑ x∈ P . f x) > (∑x ∈ P . g x)"
  shows "∃ x∈P . f x > g x "
proof (rule ccontr)
  assume CF: "¬(∃ x∈P . f x > g x)"
  then show "False" 
  proof -
    from CF have "∀ x∈ P.  f x ≤  g x" by auto
    hence "∀x.  (x∈P ⟶ f x ≤ g x)" by simp
    from this sum_mono have "(∑x∈P. f x) ≤ (∑x∈P. g x)" by metis
    thus "False" using A by arith 
  qed
qed



end