diff --git a/thys/Girth_Chromatic/Girth_Chromatic.thy b/thys/Girth_Chromatic/Girth_Chromatic.thy
--- a/thys/Girth_Chromatic/Girth_Chromatic.thy
+++ b/thys/Girth_Chromatic/Girth_Chromatic.thy
@@ -1,737 +1,737 @@
 theory Girth_Chromatic
 imports
   Ugraphs
   Girth_Chromatic_Misc
   "HOL-Probability.Probability"
   "HOL-Decision_Procs.Approximation"
 begin
 
 section \<open>Probability Space on Sets of Edges\<close>
 
 definition cylinder :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set set" where
   "cylinder S A B = {T \<in> Pow S. A \<subseteq> T \<and> B \<inter> T = {}}"
 
 lemma full_sum:
   fixes p :: real
   assumes "finite S"
   shows "(\<Sum>A\<in>Pow S. p^card A * (1 - p)^card (S - A)) = 1"
 using assms
 proof induct
   case (insert s S)
   have "inj_on (insert s) (Pow S)"
       and "\<And>x. S - insert s x = S - x"
       and "Pow S \<inter> insert s ` Pow S = {}"
       and "\<And>x. x \<in> Pow S \<Longrightarrow> card (insert s S - x) = Suc (card (S - x))"
     using insert(1-2) by (auto simp: insert_Diff_if intro!: inj_onI)
   moreover have "\<And>x. x \<subseteq> S \<Longrightarrow> card (insert s x) = Suc (card x)"
     using insert(1-2) by (subst card.insert) (auto dest: finite_subset)
   ultimately show ?case
     by (simp add: sum.reindex sum_distrib_left[symmetric] ac_simps
                   insert.hyps sum.union_disjoint Pow_insert)
 qed simp
 
 text \<open>Definition of the probability space on edges:\<close>
 locale edge_space =
   fixes n :: nat and p :: real
   assumes p_prob: "0 \<le> p" "p \<le> 1"
 begin
 
 definition S_verts :: "nat set" where
   "S_verts \<equiv> {1..n}"
 
 definition S_edges :: "uedge set" where
   "S_edges = all_edges S_verts"
 
 definition edge_ugraph :: "uedge set \<Rightarrow> ugraph" where
   "edge_ugraph es \<equiv> (S_verts, es \<inter> S_edges)"
 
 definition "P = point_measure (Pow S_edges) (\<lambda>s. p^card s * (1 - p)^card (S_edges - s))"
 
 lemma finite_verts[intro!]: "finite S_verts"
   by (auto simp: S_verts_def)
 
 lemma finite_edges[intro!]: "finite S_edges"
   by (auto simp: S_edges_def all_edges_def finite_verts)
 
 lemma finite_graph[intro!]: "finite (uverts (edge_ugraph es))"
   unfolding edge_ugraph_def by auto
 
 lemma uverts_edge_ugraph[simp]: "uverts (edge_ugraph es) = S_verts"
   by (simp add: edge_ugraph_def)
 
 lemma uedges_edge_ugraph[simp]: "uedges (edge_ugraph es) = es \<inter> S_edges"
   unfolding edge_ugraph_def by simp
 
 lemma space_eq: "space P = Pow S_edges" by (simp add: P_def space_point_measure)
 
 lemma sets_eq: "sets P = Pow (Pow S_edges)" by (simp add: P_def sets_point_measure)
 
 lemma emeasure_eq:
   "emeasure P A = (if A \<subseteq> Pow S_edges then (\<Sum>edges\<in>A. p^card edges * (1 - p)^card (S_edges - edges)) else 0)"
   using finite_edges p_prob
   by (simp add: P_def space_point_measure emeasure_point_measure_finite
     sets_point_measure emeasure_notin_sets)
 
 lemma integrable_P[intro, simp]: "integrable P (f::_ \<Rightarrow> real)"
   using finite_edges by (simp add: integrable_point_measure_finite P_def)
 
 lemma borel_measurable_P[measurable]: "f \<in> borel_measurable P"
   unfolding P_def by simp
 
 lemma prob_space_P: "prob_space P"
 proof
   show "emeasure P (space P) = 1" \<comment> \<open>Sum of probabilities equals 1\<close>
     using finite_edges by (simp add: emeasure_eq full_sum one_ereal_def space_eq)
 qed
 
 end
 
 sublocale edge_space \<subseteq> prob_space P
   by (rule prob_space_P)
 
 context edge_space
 begin
 
 lemma prob_eq:
   "prob A = (if A \<subseteq> Pow S_edges then (\<Sum>edges\<in>A. p^card edges * (1 - p)^card (S_edges - edges)) else 0)"
   using emeasure_eq[of A] p_prob unfolding emeasure_eq_measure by (simp add: sum_nonneg)
 
 lemma integral_finite_singleton: "integral\<^sup>L P f = (\<Sum>x\<in>Pow S_edges. f x * measure P {x})"
   using p_prob prob_eq unfolding P_def
   by (subst lebesgue_integral_point_measure_finite) (auto intro!: sum.cong)
 
 text \<open>Probability of cylinder sets:\<close>
 lemma cylinder_prob:
   assumes "A \<subseteq> S_edges" "B \<subseteq> S_edges" "A \<inter> B = {}"
   shows "prob (cylinder S_edges A B) = p ^ (card A) * (1 - p) ^ (card B)" (is "_ = ?pp A B")
 proof -
   have "Pow S_edges \<inter> cylinder S_edges A B = cylinder S_edges A B"
        "\<And>x. x \<in> cylinder S_edges A B \<Longrightarrow> A \<union> x = x"
        "\<And>x. x \<in> cylinder S_edges A B \<Longrightarrow> finite x"
        "\<And>x. x \<in> cylinder S_edges A B \<Longrightarrow> B \<inter> (S_edges - B - x) = {}"
        "\<And>x. x \<in> cylinder S_edges A B \<Longrightarrow> B \<union> (S_edges - B - x) = S_edges - x"
        "finite A" "finite B"
     using assms by (auto simp add: cylinder_def intro: finite_subset)
   then have "(\<Sum>T\<in>cylinder S_edges A B. ?pp T (S_edges - T))
       = (\<Sum>T \<in> cylinder S_edges A B. p^(card A + card (T - A)) * (1 - p)^(card B + card ((S_edges - B) - T)))"
     using finite_edges by (simp add: card_Un_Int)
   also have "\<dots> = ?pp A B * (\<Sum>T\<in>cylinder S_edges A B. ?pp (T - A) (S_edges - B - T))"
     by (simp add: power_add sum_distrib_left ac_simps)
   also have "\<dots> = ?pp A B"
   proof -
     have "\<And>T. T \<in> cylinder S_edges A B \<Longrightarrow> S_edges - B - T = (S_edges - A) - B - (T - A)"
          "Pow (S_edges - A - B) = (\<lambda>x. x - A) ` cylinder S_edges A B"
          "inj_on (\<lambda>x. x - A) (cylinder S_edges A B)"
          "finite (S_edges - A - B)"
       using assms by (auto simp: cylinder_def intro!: inj_onI)
     with full_sum[of "S_edges - A - B"] show ?thesis by (simp add: sum.reindex)
   qed
   finally show ?thesis by (auto simp add: prob_eq cylinder_def)
 qed
 
 lemma Markov_inequality:
   fixes a :: real and X :: "uedge set \<Rightarrow> real"
   assumes "0 < c" "\<And>x. 0 \<le> f x"
   shows "prob {x \<in> space P. c \<le> f x} \<le> (\<integral>x. f x \<partial> P) / c"
 proof -
   from assms have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>P) = (\<integral>x. f x \<partial>P)"
     by (intro nn_integral_eq_integral) auto
   with assms show ?thesis
     using nn_integral_Markov_inequality[of f "space P" P "1 / c"]
     by (simp cong: nn_integral_cong add: emeasure_eq_measure ennreal_mult[symmetric])
 qed
 
 end
 
 subsection \<open>Graph Probabilities outside of @{term Edge_Space} locale\<close>
 
 text \<open>
  These abbreviations allow a compact expression of probabilities about random
  graphs outside of the @{term Edge_Space} locale. We also transfer a few of the lemmas
  we need from the locale into the toplevel theory.
 \<close>
 
 abbreviation MGn :: "(nat \<Rightarrow> real) \<Rightarrow> nat \<Rightarrow> (uedge set) measure" where
   "MGn p n \<equiv> (edge_space.P n (p n))"
 abbreviation probGn :: "(nat \<Rightarrow> real) \<Rightarrow> nat \<Rightarrow> (uedge set \<Rightarrow> bool) \<Rightarrow> real" where
   "probGn p n P \<equiv> measure (MGn p n) {es \<in> space (MGn p n). P es}"
 
 lemma probGn_le:
   assumes p_prob: "0 < p n" "p n < 1"
   assumes sub: "\<And>n es. es \<in> space (MGn p n) \<Longrightarrow> P n es \<Longrightarrow> Q n es"
   shows "probGn p n (P n) \<le> probGn p n (Q n)"
 proof -
   from p_prob interpret E: edge_space n "p n" by unfold_locales auto
   show ?thesis
     by (auto intro!: E.finite_measure_mono sub simp: E.space_eq E.sets_eq)
 qed
 
 section \<open>Short cycles\<close>
 
 definition short_cycles :: "ugraph \<Rightarrow> nat \<Rightarrow> uwalk set" where
   "short_cycles G k \<equiv> {p \<in> ucycles G. uwalk_length p \<le> k}"
 
 text \<open>obtains a vertex in a short cycle:\<close>
 definition choose_v :: "ugraph \<Rightarrow> nat \<Rightarrow> uvert" where
   "choose_v G k \<equiv> SOME u. \<exists>p. p \<in> short_cycles G k \<and> u \<in> set p"
 
 partial_function (tailrec) kill_short :: "ugraph \<Rightarrow> nat \<Rightarrow> ugraph" where
   "kill_short G k = (if short_cycles G k = {} then G else (kill_short (G -- (choose_v G k)) k))"
 
 lemma ksc_simps[simp]:
   "short_cycles G k = {} \<Longrightarrow> kill_short G k = G"
   "short_cycles G k \<noteq> {}  \<Longrightarrow> kill_short G k = kill_short (G -- (choose_v G k)) k"
   by (auto simp: kill_short.simps)
 
 lemma
   assumes "short_cycles G k \<noteq> {}"
   shows choose_v__in_uverts: "choose_v G k \<in> uverts G" (is ?t1)
     and choose_v__in_short: "\<exists>p. p \<in> short_cycles G k \<and> choose_v G k \<in> set p" (is ?t2)
 proof -
   from assms obtain p where "p \<in> ucycles G" "uwalk_length p \<le> k"
     unfolding short_cycles_def by auto
   moreover
   then obtain u where "u \<in> set p" unfolding ucycles_def
     by (cases p) (auto simp: uwalk_length_conv)
   ultimately have "\<exists>u p. p \<in> short_cycles G k \<and> u \<in> set p"
     by (auto simp: short_cycles_def)
   then show ?t2 by (auto simp: choose_v_def intro!: someI_ex)
   then show ?t1 by (auto simp: short_cycles_def ucycles_def uwalks_def)
 qed
 
 lemma kill_step_smaller:
   assumes "short_cycles G k \<noteq> {}"
   shows "short_cycles (G -- (choose_v G k)) k \<subset> short_cycles G k"
 proof -
   let ?cv = "choose_v G k"
   from assms obtain p where "p \<in> short_cycles G k" "?cv \<in> set p"
     by atomize_elim (rule choose_v__in_short)
 
   have "short_cycles (G -- ?cv) k \<subseteq> short_cycles G k"
   proof
     fix p assume "p \<in> short_cycles (G -- ?cv) k"
     then show "p \<in> short_cycles G k"
       unfolding short_cycles_def ucycles_def uwalks_def
       using edges_Gu[of G ?cv] by (auto simp: verts_Gu)
   qed
   moreover have "p \<notin> short_cycles (G -- ?cv) k"
     using \<open>?cv \<in> set p\<close> by (auto simp: short_cycles_def ucycles_def uwalks_def verts_Gu)
   ultimately show ?thesis using \<open>p \<in> short_cycles G k\<close> by auto
 qed
 
 text \<open>Induction rule for @{term kill_short}:\<close>
 lemma kill_short_induct[consumes 1, case_names empty kill_vert]:
   assumes fin: "finite (uverts G)"
   assumes a_empty: "\<And>G. short_cycles G k = {} \<Longrightarrow> P G k"
   assumes a_kill: "\<And>G. finite (short_cycles G k) \<Longrightarrow> short_cycles G k \<noteq> {}
     \<Longrightarrow> P (G -- (choose_v G k)) k \<Longrightarrow> P G k"
   shows "P G k"
 proof -
   have "finite (short_cycles G k)"
     using finite_ucycles[OF fin] by (auto simp: short_cycles_def)
   then show ?thesis
     by (induct "short_cycles G k" arbitrary: G rule: finite_psubset_induct)
       (metis kill_step_smaller a_kill a_empty)
 qed
 
 text \<open>Large Girth (after @{term kill_short}):\<close>
 lemma kill_short_large_girth:
   assumes "finite (uverts G)"
   shows "k < girth (kill_short G k)"
 using assms
 proof (induct G k rule: kill_short_induct)
   case (empty G)
   then have "\<And>p. p \<in> ucycles G \<Longrightarrow> k < enat (uwalk_length p)"
     by (auto simp: short_cycles_def)
   with empty show ?case by (auto simp: girth_def intro: enat_less_INF_I)
 qed simp
 
 text \<open>Order of graph (after @{term kill_short}):\<close>
 lemma kill_short_order_of_graph:
   assumes "finite (uverts G)"
   shows "card (uverts G) - card (short_cycles G k) \<le> card (uverts (kill_short G k))"
 using assms assms
 proof (induct G k rule: kill_short_induct)
   case (kill_vert G)
   let ?oG = "G -- (choose_v G k)"
 
   have "finite (uverts ?oG)"
     using kill_vert by (auto simp: remove_vertex_def)
   moreover
   have "uverts (kill_short G k) = uverts (kill_short ?oG k)"
     using kill_vert by simp
   moreover
   have "card (uverts G) = Suc (card (uverts ?oG))"
     using choose_v__in_uverts kill_vert
     by (simp add: remove_vertex_def card_Suc_Diff1 del: card_Diff_insert)
   moreover
   have "card (short_cycles ?oG k) < card (short_cycles G k)"
     by (intro psubset_card_mono kill_vert.hyps kill_step_smaller)
   ultimately show ?case using kill_vert.hyps by presburger
 qed simp
 
 text \<open>Independence number (after @{term kill_short}):\<close>
 lemma kill_short_\<alpha>:
   assumes "finite (uverts G)"
   shows "\<alpha> (kill_short G k) \<le> \<alpha> G"
 using assms
 proof (induct G k rule: kill_short_induct)
   case (kill_vert G)
   note kill_vert(3)
   also have "\<alpha> (G -- (choose_v G k)) \<le> \<alpha> G" by (rule \<alpha>_remove_le)
   finally show ?case using kill_vert by simp
 qed simp
 
 text \<open>Wellformedness (after @{term kill_short}):\<close>
 lemma kill_short_uwellformed:
   assumes "finite (uverts G)" "uwellformed G"
   shows "uwellformed (kill_short G k)"
 using assms
 proof (induct G k rule: kill_short_induct)
   case (kill_vert G)
   from kill_vert.prems have "uwellformed (G -- (choose_v G k))"
     by (auto simp: uwellformed_def remove_vertex_def)
   with kill_vert.hyps show ?case by simp
 qed simp
 
 
 section \<open>The Chromatic-Girth Theorem\<close>
 
 text \<open>Probability of Independent Edges:\<close>
 lemma (in edge_space) random_prob_independent:
   assumes "n \<ge> k" "k \<ge> 2"
   shows "prob {es \<in> space P. k \<le> \<alpha> (edge_ugraph es)}
     \<le> (n choose k)*(1-p)^(k choose 2)"
 proof -
   let "?k_sets" = "{vs. vs \<subseteq> S_verts \<and> card vs = k}"
 
   { fix vs assume A: "vs \<in> ?k_sets"
     then have B: "all_edges vs \<subseteq> S_edges"
       unfolding all_edges_def S_edges_def by blast
 
     have "{es \<in> space P. vs \<in> independent_sets (edge_ugraph es)}
         = cylinder S_edges {} (all_edges vs)" (is "?L = _")
       using A by (auto simp: independent_sets_def edge_ugraph_def space_eq cylinder_def)
     then have "prob ?L = (1-p)^(k choose 2)"
       using A B finite by (auto simp: cylinder_prob card_all_edges dest: finite_subset)
   }
   note prob_k_indep = this
     \<comment> \<open>probability that a fixed set of k vertices is independent in a random graph\<close>
 
   have "{es \<in> space P. k \<in> card ` independent_sets (edge_ugraph es)}
     = (\<Union>vs \<in> ?k_sets. {es \<in> space P. vs \<in> independent_sets (edge_ugraph es)})" (is "?L = ?R")
     unfolding image_def space_eq independent_sets_def by auto
   then have "prob ?L \<le> (\<Sum>vs \<in> ?k_sets. prob {es \<in> space P. vs \<in> independent_sets (edge_ugraph es)})"
     by (auto intro!: finite_measure_subadditive_finite simp: space_eq sets_eq)
   also have "\<dots> = (n choose k)*((1 - p) ^ (k choose 2))"
     by (simp add: prob_k_indep S_verts_def n_subsets)
   finally show ?thesis using \<open>k \<ge> 2\<close> by (simp add: le_\<alpha>_iff)
 qed
 
 text \<open>Almost never many independent edges:\<close>
 lemma almost_never_le_\<alpha>:
   fixes k :: nat
     and p :: "nat \<Rightarrow> real"
   assumes p_prob: "\<forall>\<^sup>\<infinity> n. 0 < p n \<and> p n < 1"
   assumes [arith]: "k > 0"
   assumes N_prop: "\<forall>\<^sup>\<infinity> n. (6 * k * ln n)/n \<le> p n"
   shows "(\<lambda>n. probGn p n (\<lambda>es. 1/2*n/k \<le> \<alpha> (edge_space.edge_ugraph n es))) \<longlonglongrightarrow> 0"
     (is "(\<lambda>n. ?prob_fun n) \<longlonglongrightarrow> 0")
 proof -
   let "?prob_fun_raw n" = "probGn p n (\<lambda>es. nat(ceiling (1/2*n/k)) \<le> \<alpha> (edge_space.edge_ugraph n es))"
 
   define r where "r n = 1 / 2 * n / k" for n :: nat
   let ?nr = "\<lambda>n. nat(ceiling (r n))"
 
   have r_pos: "\<And>n. 0 < n \<Longrightarrow> 0 < r n " by (auto simp: r_def field_simps)
 
   have nr_bounds: "\<forall>\<^sup>\<infinity> n. 2 \<le> ?nr n \<and> ?nr n \<le> n"
     by (intro eventually_sequentiallyI[of "4 * k"])
        (simp add: r_def nat_ceiling_le_eq le_natceiling_iff field_simps)
 
   from nr_bounds p_prob have ev_prob_fun_raw_le:
     "\<forall>\<^sup>\<infinity> n. probGn p n (\<lambda>es. ?nr n\<le> \<alpha> (edge_space.edge_ugraph n es))
       \<le> (n * exp (- p n * (real (?nr n) - 1) / 2)) powr ?nr n"
     (is "\<forall>\<^sup>\<infinity> n. ?prob_fun_raw_le n")
   proof (rule eventually_elim2)
     fix n :: nat assume A: "2 \<le> ?nr n \<and> ?nr n \<le> n" "0 < p n \<and>p n < 1"
     then interpret pG: edge_space n "p n" by unfold_locales auto
 
     have r: "real (?nr n - Suc 0) = real (?nr n) - Suc 0" using A by auto
 
     have [simp]: "n>0" using A by linarith
     have "probGn p n (\<lambda>es. ?nr n \<le> \<alpha> (edge_space.edge_ugraph n es))
         \<le> (n choose ?nr n) * (1 - p n)^(?nr n choose 2)"
       using A by (auto intro: pG.random_prob_independent)
     also have "\<dots> \<le> n powr ?nr n * (1 - p n) powr (?nr n choose 2)"
       using A  by (simp add: powr_realpow of_nat_power [symmetric] binomial_le_pow  del: of_nat_power)
     also have "\<dots> = n powr ?nr n * (1 - p n) powr (?nr n * (?nr n - 1) / 2)"
       by (cases "even (?nr n - 1)")
-        (auto simp add: n_choose_2_nat real_of_nat_div)
+        (auto simp add: choose_two real_of_nat_div)
     also have "\<dots> = n powr ?nr n * ((1 - p n) powr ((?nr n - 1) / 2)) powr ?nr n"
       by (auto simp add: powr_powr r ac_simps)
     also have "\<dots> \<le> (n * exp (- p n * (?nr n - 1) / 2)) powr ?nr n"
     proof -
       have "(1 - p n) powr ((?nr n - 1) / 2) \<le> exp (- p n) powr ((?nr n - 1) / 2)"
         using A by (auto simp: powr_mono2 diff_conv_add_uminus simp del: add_uminus_conv_diff)
       also have "\<dots> = exp (- p n * (?nr n - 1) / 2)" by (auto simp: powr_def)
       finally show ?thesis
         using A by (auto simp: powr_mono2 powr_mult)
     qed
     finally show "probGn p n (\<lambda>es. ?nr n \<le> \<alpha> (edge_space.edge_ugraph n es))
       \<le> (n * exp (- p n * (real (?nr n) - 1) / 2)) powr ?nr n"
       using A r by simp
   qed
 
   from p_prob N_prop
   have ev_expr_bound: "\<forall>\<^sup>\<infinity> n. n * exp (-p n * (real (?nr n) - 1) / 2) \<le> (exp 1 / n) powr (1 / 2)"
   proof (elim eventually_rev_mp, intro eventually_sequentiallyI conjI impI)
     fix n assume n_bound[arith]: "2 \<le> n"
       and p_bound: "0 < p n \<and> p n < 1" "(6 * k * ln n) / n \<le> p n"
     have r_bound: "r n \<le> ?nr n" by (rule real_nat_ceiling_ge)
 
     have "n * exp (-p n * (real (?nr n)- 1) / 2) \<le> n * exp (- 3 / 2 * ln n + p n / 2)"
     proof -
       have "0 < ln n" using "n_bound" by auto
       then have "(3 / 2) * ln n \<le> ((6 * k * ln n) / n) * (?nr n / 2)"
         using r_bound le_of_int_ceiling[of "n/2*k"]
         by (simp add: r_def field_simps del: le_of_int_ceiling)
       also have "\<dots> \<le> p n * (?nr n / 2)"
         using n_bound p_bound r_bound r_pos[of n] by (auto simp: field_simps)
       finally show ?thesis using r_bound by (auto simp: field_simps)
     qed
     also have "\<dots> \<le> n * n powr (- 3 / 2) * exp 1 powr (1 / 2)"
       using p_bound by (simp add: powr_def exp_add [symmetric])
     also have "\<dots> \<le> n powr (-1 / 2) * exp 1 powr (1 / 2)" by (simp add: powr_mult_base)
     also have "\<dots> = (exp 1 / n) powr (1/2)"
       by (simp add: powr_divide powr_minus_divide)
     finally show "n * exp (- p n * (real (?nr n) - 1) / 2) \<le> (exp 1 / n) powr (1 / 2)" .
   qed
 
   have ceil_bound: "\<And>G n. 1/2*n/k \<le> \<alpha> G \<longleftrightarrow> nat(ceiling (1/2*n/k)) \<le> \<alpha> G"
     by (case_tac "\<alpha> G") (auto simp: nat_ceiling_le_eq)
 
   show ?thesis
   proof (unfold ceil_bound, rule real_tendsto_sandwich)
     show "(\<lambda>n. 0) \<longlonglongrightarrow> 0"
         "(\<lambda>n. (exp 1 / n) powr (1 / 2)) \<longlonglongrightarrow> 0"
         "\<forall>\<^sup>\<infinity> n. 0 \<le> ?prob_fun_raw n"
       using p_prob by (auto intro: measure_nonneg LIMSEQ_inv_powr elim: eventually_mono)
   next
     from nr_bounds ev_expr_bound ev_prob_fun_raw_le
     show "\<forall>\<^sup>\<infinity> n. ?prob_fun_raw n \<le> (exp 1 / n) powr (1 / 2)"
     proof (elim eventually_rev_mp, intro eventually_sequentiallyI impI conjI)
       fix n assume A: "3 \<le> n"
         and nr_bounds: "2 \<le> ?nr n \<and> ?nr n \<le> n"
         and prob_fun_raw_le: "?prob_fun_raw_le n"
         and expr_bound: "n * exp (- p n * (real (nat(ceiling (r n))) - 1) / 2) \<le> (exp 1 / n) powr (1 / 2)"
 
       have "exp 1 < (3 :: real)" by (approximation 6)
       then have "(exp 1 / n) powr (1 / 2) \<le> 1 powr (1 / 2)"
         using A by (intro powr_mono2) (auto simp: field_simps)
       then have ep_bound: "(exp 1 / n) powr (1 / 2) \<le> 1" by simp
 
       have "?prob_fun_raw n \<le> (n * exp (- p n * (real (?nr n) - 1) / 2)) powr (?nr n)"
         using prob_fun_raw_le by (simp add: r_def)
       also have "\<dots> \<le> ((exp 1 / n) powr (1 / 2)) powr ?nr n"
         using expr_bound A by (auto simp: powr_mono2)
       also have "\<dots> \<le> ((exp 1 / n) powr (1 / 2))"
         using nr_bounds ep_bound A by (auto simp: powr_le_one_le)
       finally show "?prob_fun_raw n \<le> (exp 1 / n) powr (1 / 2)" .
     qed
   qed
 qed
 
 text \<open>Mean number of k-cycles in a graph. (Or rather of paths describing a circle of length @{term k}):\<close>
 lemma (in edge_space) mean_k_cycles:
   assumes "3 \<le> k" "k < n"
   shows "(\<integral>es. card {c \<in> ucycles (edge_ugraph es). uwalk_length c = k} \<partial> P)
     = of_nat (fact n div fact (n - k)) * p ^ k"
 proof -
   let ?k_cycle = "\<lambda>es c k. c \<in> ucycles (edge_ugraph es) \<and> uwalk_length c = k"
   define C where "C k = {c. ?k_cycle S_edges c k}" for k
     \<comment> \<open>@{term "C k"} is the set of all possible cycles of size @{term k} in @{term "edge_ugraph S_edges"}\<close>
   define XG  where "XG es = {c. ?k_cycle es c k}" for es
     \<comment> \<open>@{term "XG es"} is the set of cycles contained in a @{term "edge_ugraph es"}\<close>
   define XC where "XC c = {es \<in> space P. ?k_cycle es c k}" for c
     \<comment> \<open>"@{term "XC c"} is the set of graphs (edge sets) containing a cycle c"\<close>
   then have XC_in_sets: "\<And>c. XC c \<in> sets P"
       and XC_cyl: "\<And>c. c \<in> C k \<Longrightarrow> XC c = cylinder S_edges (set (uwalk_edges c)) {}"
     by (auto simp: ucycles_def space_eq uwalks_def C_def cylinder_def sets_eq)
 
   have "(\<integral>es. card {c \<in> ucycles (edge_ugraph es). uwalk_length c = k} \<partial> P)
       =  (\<Sum>x\<in>space P. card (XG x) * prob {x})"
     by (simp add: XG_def integral_finite_singleton space_eq)
   also have "\<dots> = (\<Sum>c\<in>C k. prob (cylinder S_edges (set (uwalk_edges c)) {}))"
   proof -
     have XG_Int_C: "\<And>s. s \<in> space P \<Longrightarrow> C k \<inter> XG s = XG s"
       unfolding XG_def C_def ucycles_def uwalks_def edge_ugraph_def by auto
     have fin_XC: "\<And>k. finite (XC k)" and fin_C: "finite (C k)"
       unfolding C_def XC_def by (auto simp: finite_edges space_eq intro!: finite_ucycles)
 
     have "(\<Sum>x\<in>space P. card (XG x) * prob {x}) = (\<Sum>x\<in>space P. (\<Sum>c \<in> XG x. prob {x}))"
       by simp
     also have "\<dots> = (\<Sum>x\<in>space P. (\<Sum>c \<in> C k. if c \<in> XG x then prob {x} else 0))"
       using fin_C by (simp add: sum.If_cases) (simp add: XG_Int_C)
     also have "\<dots> = (\<Sum>c \<in> C k. (\<Sum> x \<in> space P \<inter> XC c. prob {x}))"
       using finite_edges by (subst sum.swap) (simp add: sum.inter_restrict XG_def XC_def space_eq)
     also have "\<dots> = (\<Sum>c \<in> C k. prob (XC c))"
       using fin_XC XC_in_sets
       by (auto simp add: prob_eq sets_eq space_eq intro!: sum.cong)
     finally show ?thesis by (simp add: XC_cyl)
   qed
   also have "\<dots> = (\<Sum>c\<in>C k. p ^ k)"
   proof -
     have "\<And>x. x \<in> C k \<Longrightarrow> card (set (uwalk_edges x)) = uwalk_length x"
       by (auto simp: uwalk_length_def C_def ucycles_distinct_edges intro: distinct_card)
     then show ?thesis by (auto simp: C_def ucycles_def uwalks_def cylinder_prob)
   qed
   also have "\<dots> = of_nat (fact n div fact (n - k)) * p ^ k"
   proof -
     have inj_last_Cons: "\<And>A. inj_on (\<lambda>es. last es # es) A" by (rule inj_onI) simp
     { fix xs A assume "3 \<le> length xs - Suc 0" "hd xs = last xs"
       then have "xs \<in> (\<lambda>xs. last xs # xs) ` A \<longleftrightarrow> tl xs \<in> A"
         by (cases xs) (auto simp: inj_image_mem_iff[OF inj_last_Cons] split: if_split_asm) }
     note image_mem_iff_inst = this
 
     { fix xs have "xs \<in> uwalks (edge_ugraph S_edges) \<Longrightarrow> set (tl xs) \<subseteq> S_verts"
         unfolding uwalks_def by (induct xs) auto }
     moreover
     { fix xs assume "set xs \<subseteq> S_verts" "2 \<le> length xs" "distinct xs"
       then have "(last xs # xs) \<in> uwalks (edge_ugraph S_edges)"
       proof (induct xs rule: uwalk_edges.induct)
         case (3 x y ys)
         have S_edges_memI: "\<And>x y. x \<in> S_verts \<Longrightarrow> y \<in> S_verts \<Longrightarrow> x \<noteq> y \<Longrightarrow> {x, y} \<in> S_edges"
           unfolding S_edges_def all_edges_def image_def by auto
 
         have "ys \<noteq> [] \<Longrightarrow> set ys \<subseteq> S_verts \<Longrightarrow> last ys \<in> S_verts"  by auto
         with 3 show ?case
           by (auto simp add: uwalks_def Suc_le_eq intro: S_edges_memI)
       qed simp_all}
     moreover note \<open>3 \<le> k\<close>
     ultimately
     have "C k = (\<lambda>xs. last xs # xs) ` {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> S_verts}"
       by (auto simp: C_def ucycles_def uwalk_length_conv image_mem_iff_inst)
     moreover have "card S_verts = n" by (simp add: S_verts_def)
     ultimately have "card (C k) = fact n div fact (n - k)"
       using \<open>k < n\<close>
       by (simp add: card_image[OF inj_last_Cons] card_lists_distinct_length_eq' fact_div_fact)
     then show ?thesis by simp
   qed
   finally show ?thesis by simp
 qed
 
 text \<open>Girth-Chromatic number theorem:\<close>
 theorem girth_chromatic:
   fixes l :: nat
   shows "\<exists>G. uwellformed G \<and> l < girth G \<and> l < chromatic_number G"
 proof -
   define k where "k = max 3 l"
   define \<epsilon> where "\<epsilon> = 1 / (2 * k)"
   define p where "p n = real n powr (\<epsilon> - 1)" for n :: nat
 
   let ?ug = edge_space.edge_ugraph
 
   define short_count where "short_count g = card (short_cycles g k)" for g
     \<comment> \<open>This random variable differs from the one used in the proof of theorem 11.2.2,
           as we count the number of paths describing a circle, not the circles themselves\<close>
 
   from k_def have "3 \<le> k" "l \<le> k" by auto
   from \<open>3 \<le> k\<close> have \<epsilon>_props: "0 < \<epsilon>" "\<epsilon> < 1 / k" "\<epsilon> < 1" by (auto simp: \<epsilon>_def field_simps)
 
   have ev_p: "\<forall>\<^sup>\<infinity> n. 0 < p n \<and> p n < 1"
   proof (rule eventually_sequentiallyI)
     fix n :: nat assume "2 \<le> n"
     with \<open>\<epsilon> < 1\<close> have "n powr (\<epsilon> - 1) < 1" by (auto intro!: powr_less_one)
     then show "0 < p n \<and> p n < 1" using \<open>2 \<le> n\<close>
       by (auto simp: p_def)
   qed
   then
   have prob_short_count_le: "\<forall>\<^sup>\<infinity> n. probGn p n (\<lambda>es. (real n/2) \<le> short_count (?ug n es))
       \<le> 2 * (k - 2) * n powr (\<epsilon> * k - 1)"  (is "\<forall>\<^sup>\<infinity> n. ?P n")
   proof (elim eventually_rev_mp, intro eventually_sequentiallyI impI)
     fix n :: nat assume A: "Suc k \<le> n" "0 < p n \<and> p n < 1"
     then interpret pG: edge_space n "p n" by unfold_locales auto
     have "1 \<le> n" using A by auto
 
     define mean_short_count where "mean_short_count = (\<integral>es. short_count (?ug n es) \<partial> pG.P)"
 
     have mean_short_count_le: "mean_short_count \<le> (k - 2) * n powr (\<epsilon> * k)"
     proof -
       have small_empty: "\<And>es k. k \<le> 2 \<Longrightarrow> short_cycles (edge_space.edge_ugraph n es) k = {}"
           by (auto simp add: short_cycles_def ucycles_def)
       have short_count_conv: "\<And>es. short_count (?ug n es) = (\<Sum>i=3..k. real (card {c \<in> ucycles (?ug n es). uwalk_length c = i}))"
       proof (unfold short_count_def, induct k)
         case 0 with small_empty show ?case by auto
       next
         case (Suc k)
         show ?case proof (cases "Suc k \<le> 2")
           case True with small_empty show ?thesis by auto
         next
           case False
           have "{c \<in> ucycles (?ug n es). uwalk_length c \<le> Suc k}
               = {c \<in> ucycles (?ug n es). uwalk_length c \<le> k} \<union> {c \<in> ucycles (?ug n es). uwalk_length c = Suc k}"
             by auto
           moreover
           have "finite (uverts (edge_space.edge_ugraph n es))" by auto
           ultimately
           have "card {c \<in> ucycles (?ug n es). uwalk_length c \<le> Suc k}
             = card {c \<in> ucycles (?ug n es). uwalk_length c \<le> k} + card {c \<in> ucycles (?ug n es). uwalk_length c = Suc k}"
             using finite_ucycles by (subst card_Un_disjoint[symmetric]) auto
           then show ?thesis
             using Suc False unfolding short_cycles_def by (auto simp: not_le)
         qed
       qed
 
       have "mean_short_count = (\<Sum>i=3..k. \<integral>es. card {c \<in> ucycles (?ug n es). uwalk_length c = i} \<partial> pG.P)"
         unfolding mean_short_count_def short_count_conv
         by (subst Bochner_Integration.integral_sum) (auto intro: pG.integral_finite_singleton)
       also have "\<dots> = (\<Sum>i\<in>{3..k}. of_nat (fact n div fact (n - i)) * p n ^ i)"
         using A by (simp add: pG.mean_k_cycles)
       also have "\<dots> \<le> (\<Sum> i\<in>{3..k}. n ^ i * p n ^ i)"
         apply (rule sum_mono)
         by (meson A fact_div_fact_le_pow  Suc_leD atLeastAtMost_iff of_nat_le_iff order_trans mult_le_cancel_iff1 zero_less_power)
       also have "... \<le> (\<Sum> i\<in>{3..k}. n powr (\<epsilon> * k))"
         using \<open>1 \<le> n\<close> \<open>0 < \<epsilon>\<close> A
         by (intro sum_mono) (auto simp: p_def field_simps powr_mult_base powr_powr
           powr_realpow[symmetric] powr_mult[symmetric] powr_add[symmetric])
       finally show ?thesis by simp
     qed
 
     have "pG.prob {es \<in> space pG.P. n/2 \<le> short_count (?ug n es)} \<le> mean_short_count / (n/2)"
       unfolding mean_short_count_def using \<open>1 \<le> n\<close>
       by (intro pG.Markov_inequality) (auto simp: short_count_def)
     also have "\<dots> \<le> 2 * (k - 2) * n powr (\<epsilon> * k - 1)"
     proof -
       have "mean_short_count / (n / 2) \<le> 2 * (k - 2) * (1 / n powr 1) * n powr (\<epsilon> * k)"
         using mean_short_count_le \<open>1 \<le> n\<close> by (simp add: field_simps)
       then show ?thesis by (simp add: powr_diff algebra_simps)
     qed
     finally show "?P n" .
   qed
 
   define pf_short_count pf_\<alpha>
     where "pf_short_count n = probGn p n (\<lambda>es. n/2 \<le> short_count (?ug n es))"
       and "pf_\<alpha> n = probGn p n (\<lambda>es. 1/2 * n/k \<le> \<alpha> (edge_space.edge_ugraph n es))"
     for n
 
   have ev_short_count_le: "\<forall>\<^sup>\<infinity> n. pf_short_count n < 1 / 2"
   proof -
     have "\<epsilon> * k - 1 < 0"
       using \<epsilon>_props \<open>3 \<le> k\<close> by (auto simp: field_simps)
     then have "(\<lambda>n. 2 * (k - 2) * n powr (\<epsilon> * k - 1)) \<longlonglongrightarrow> 0" (is "?bound \<longlonglongrightarrow> 0")
       by (intro tendsto_mult_right_zero LIMSEQ_neg_powr)
     then have "\<forall>\<^sup>\<infinity> n. dist (?bound n) 0  < 1 / 2"
       by (rule tendstoD) simp
     with prob_short_count_le show ?thesis
       by (rule eventually_elim2) (auto simp: dist_real_def pf_short_count_def)
   qed
 
   have lim_\<alpha>: "pf_\<alpha> \<longlonglongrightarrow> 0"
   proof -
     have "0 < k" using \<open>3 \<le> k\<close> by simp
 
     have "\<forall>\<^sup>\<infinity> n. (6*k) * ln n / n \<le> p n \<longleftrightarrow> (6*k) * ln n * n powr - \<epsilon> \<le> 1"
     proof (rule eventually_sequentiallyI)
      fix n :: nat assume "1 \<le> n"
       then have "(6 * k) * ln n / n \<le> p n \<longleftrightarrow> (6*k) * ln n * (n powr - 1) \<le> n powr (\<epsilon> - 1)"
         by  (subst powr_minus) (simp add: divide_inverse p_def)
       also have "\<dots> \<longleftrightarrow> (6*k) * ln n * ((n powr - 1) / (n powr (\<epsilon> - 1))) \<le> n powr (\<epsilon> - 1) / (n powr (\<epsilon> - 1))"
         using \<open>1 \<le> n\<close> by (auto simp: field_simps)
       also have "\<dots> \<longleftrightarrow> (6*k) * ln n * n powr - \<epsilon> \<le> 1"
         by (simp add: powr_diff [symmetric] )
       finally show "(6*k) * ln n / n \<le> p n \<longleftrightarrow> (6*k) * ln n * n powr - \<epsilon> \<le> 1" .
     qed
     then have "(\<forall>\<^sup>\<infinity> n. (6 * k) * ln n / real n \<le> p n)
         \<longleftrightarrow> (\<forall>\<^sup>\<infinity> n. (6*k) * ln n * n powr - \<epsilon> \<le> 1)"
       by (rule eventually_subst)
     also have "\<forall>\<^sup>\<infinity> n. (6*k) * ln n * n powr - \<epsilon> \<le> 1"
     proof -
       { fix n :: nat assume "0 < n"
         have "ln (real n) \<le> n powr (\<epsilon>/2) / (\<epsilon>/2)"
           using \<open>0 < n\<close> \<open>0 < \<epsilon>\<close> by (intro ln_powr_bound) auto
         also have "\<dots> \<le> 2/\<epsilon> * n powr (\<epsilon>/2)" by (auto simp: field_simps)
         finally have "(6*k) * ln n * (n powr - \<epsilon>)  \<le> (6*k) * (2/\<epsilon> * n powr (\<epsilon>/2)) * (n powr - \<epsilon>)"
           using \<open>0 < n\<close> \<open>0 < k\<close> by (intro mult_right_mono mult_left_mono) auto
         also have "\<dots> = 12*k/\<epsilon> * n powr (-\<epsilon>/2)"
           unfolding divide_inverse
           by (auto simp: field_simps powr_minus[symmetric] powr_add[symmetric])
         finally have "(6*k) * ln n * (n powr - \<epsilon>) \<le> 12*k/\<epsilon> * n powr (-\<epsilon>/2)" .
       }
       then have "\<forall>\<^sup>\<infinity> n. (6*k) * ln n * (n powr - \<epsilon>) \<le> 12*k/\<epsilon> * n powr (-\<epsilon>/2)"
         by (intro eventually_sequentiallyI[of 1]) auto
       also have "\<forall>\<^sup>\<infinity> n. 12*k/\<epsilon> * n powr (-\<epsilon>/2) \<le> 1"
       proof -
         have "(\<lambda>n. 12*k/\<epsilon> * n powr (-\<epsilon>/2)) \<longlonglongrightarrow> 0"
           using \<open>0 < \<epsilon>\<close> by (intro tendsto_mult_right_zero LIMSEQ_neg_powr) auto
         then show ?thesis
           using \<open>0 < \<epsilon>\<close> by - (drule tendstoD[where e=1], auto elim: eventually_mono)
       qed
       finally (eventually_le_le) show ?thesis .
     qed
     finally have "\<forall>\<^sup>\<infinity> n. real (6 * k) * ln (real n) / real n \<le> p n" .
     with ev_p \<open>0 < k\<close> show ?thesis unfolding pf_\<alpha>_def by (rule almost_never_le_\<alpha>)
   qed
 
   from ev_short_count_le lim_\<alpha>[THEN tendstoD, of "1/2"] ev_p
   have "\<forall>\<^sup>\<infinity> n. 0 < p n \<and> p n < 1 \<and> pf_short_count n < 1/2 \<and> pf_\<alpha> n < 1/2"
     by simp (elim eventually_rev_mp, auto simp: eventually_sequentially dist_real_def)
   then obtain n where "0 < p n" "p n < 1" and [arith]: "0 < n"
       and probs: "pf_short_count n < 1/2" "pf_\<alpha> n < 1/2"
     by (auto simp: eventually_sequentially)
   then interpret ES: edge_space n "(p n)" by unfold_locales auto
 
   have rest_compl: "\<And>A P. A - {x\<in>A. P x} = {x\<in>A. \<not>P x}" by blast
 
   from probs have "ES.prob ({es \<in> space ES.P. n/2 \<le> short_count (?ug n es)}
       \<union> {es \<in> space ES.P. 1/2 * n/k \<le> \<alpha> (?ug n es)}) \<le> pf_short_count n + pf_\<alpha> n"
     unfolding pf_short_count_def pf_\<alpha>_def  by (subst ES.finite_measure_subadditive) auto
   also have "\<dots> < 1" using probs by auto
   finally have "0 < ES.prob (space ES.P - ({es \<in> space ES.P. n/2 \<le> short_count (?ug n es)}
       \<union> {es \<in> space ES.P. 1/2 * n/k \<le> \<alpha> (?ug n es)}))" (is "0 < ES.prob ?S")
     by (subst ES.prob_compl) auto
   also have "?S = {es \<in> space ES.P. short_count (?ug n es) < n/2 \<and> \<alpha> (?ug n es) < 1/2* n/k}" (is "\<dots> = ?C")
     by (auto simp: not_less rest_compl)
   finally have "?C \<noteq> {}" by (intro notI) (simp only:, auto)
   then obtain es where es_props: "es \<in> space ES.P"
       "short_count (?ug n es) < n/2" "\<alpha> (?ug n es) < 1/2 * n/k"
     by auto
     \<comment> \<open>now we obtained a high colored graph (few independent nodes) with almost no short cycles\<close>
 
   define G where "G = ?ug n es"
   define H where "H = kill_short G k"
 
   have G_props: "uverts G = {1..n}" "finite (uverts G)" "short_count G < n/2" "\<alpha> G < 1/2 * n/k"
     unfolding G_def using es_props by (auto simp: ES.S_verts_def)
 
   have "uwellformed G" by (auto simp: G_def uwellformed_def all_edges_def ES.S_edges_def)
   with G_props have T1: "uwellformed H" unfolding H_def by (intro kill_short_uwellformed)
 
   have "enat l \<le> enat k" using \<open>l \<le> k\<close> by simp
   also have "\<dots> < girth H" using G_props by (auto simp: kill_short_large_girth H_def)
   finally have T2: "l < girth H" .
 
   have card_H: "n/2 \<le> card (uverts H)"
     using G_props es_props kill_short_order_of_graph[of G k] by (simp add: short_count_def H_def)
 
   then have uverts_H: "uverts H \<noteq> {}" "0 < card (uverts H)" by auto
   then have "0 < \<alpha> H" using zero_less_\<alpha> uverts_H by auto
 
   have \<alpha>_HG: "\<alpha> H \<le> \<alpha> G"
     unfolding H_def G_def by (auto intro: kill_short_\<alpha>)
 
   have "enat l \<le> ereal k" using \<open>l \<le> k\<close> by auto
   also have "\<dots> < (n/2) / \<alpha> G" using G_props \<open>3 \<le> k\<close>
     by (cases "\<alpha> G") (auto simp: field_simps)
   also have "\<dots> \<le> (n/2) / \<alpha> H" using \<alpha>_HG \<open>0 < \<alpha> H\<close>
     by (auto simp: ereal_of_enat_pushout intro!: ereal_divide_left_mono)
   also have "\<dots> \<le> card (uverts H) / \<alpha> H" using card_H \<open>0 < \<alpha> H\<close>
     by (auto intro!: ereal_divide_right_mono)
   also have "\<dots> \<le> chromatic_number H" using uverts_H T1 by (intro chromatic_lb) auto
   finally have T3: "l < chromatic_number H"
     by (simp del: ereal_of_enat_simps)
 
   from T1 T2 T3 show ?thesis by fast
 qed
 
 end
diff --git a/thys/Girth_Chromatic/Girth_Chromatic_Misc.thy b/thys/Girth_Chromatic/Girth_Chromatic_Misc.thy
--- a/thys/Girth_Chromatic/Girth_Chromatic_Misc.thy
+++ b/thys/Girth_Chromatic/Girth_Chromatic_Misc.thy
@@ -1,189 +1,122 @@
 theory Girth_Chromatic_Misc
 imports
   Main
   "HOL-Library.Extended_Real"
 begin
 
 section \<open>Auxilliary lemmas and setup\<close>
 
 text \<open>
   This section contains facts about general concepts which are not directly
   connected to the proof of the Chromatic-Girth theorem. At some point in time,
   most of them could be moved to the Isabelle base library.
 
   Also, a little bit of setup happens.
 \<close>
 
 subsection \<open>Numbers\<close>
 
 lemma enat_in_Inf:
   fixes S :: "enat set"
   assumes "Inf S \<noteq> top"
   shows "Inf S \<in> S"
-proof (rule ccontr)
-  assume A: "~?thesis"
-
-  obtain n where Inf_conv: "Inf S = enat n" using assms by (auto simp: top_enat_def)
-  { fix s assume "s \<in> S"
-    then have "Inf S \<le> s" by (rule complete_lattice_class.Inf_lower)
-    moreover have "Inf S \<noteq> s" using A \<open>s \<in> S\<close> by auto
-    ultimately have "Inf S < s" by simp
-    with Inf_conv have "enat (Suc n) \<le> s" by (cases s) auto
-  }
-  then have "enat (Suc n) \<le> Inf S" by (simp add: le_Inf_iff)
-  with Inf_conv show False by auto
-qed
+  using assms wellorder_InfI by auto
 
 lemma enat_in_INF:
   fixes f :: "'a \<Rightarrow> enat"
-  assumes "(INF x\<in> S. f x) \<noteq> top"
-  obtains x where "x \<in> S" and "(INF x\<in> S. f x) = f x"
-proof -
-  from assms have "(INF x\<in> S. f x) \<in> f ` S"
-    using enat_in_Inf [of "f ` S"] by auto
-  then obtain x where "x \<in> S" "(INF x\<in> S. f x) = f x" by auto
-  then show ?thesis ..
-qed
+  assumes "(INF x\<in>S. f x) \<noteq> top"
+  obtains x where "x \<in> S" and "(INF x\<in>S. f x) = f x"
+  by (meson assms enat_in_Inf imageE)
 
 lemma enat_less_INF_I:
   fixes f :: "'a \<Rightarrow> enat"
   assumes not_inf: "x \<noteq> \<infinity>" and less: "\<And>y. y \<in> S \<Longrightarrow> x < f y"
   shows "x < (INF y\<in>S. f y)"
   using assms by (auto simp: Suc_ile_eq[symmetric] INF_greatest)
 
 lemma enat_le_Sup_iff:
   "enat k \<le> Sup M \<longleftrightarrow> k = 0 \<or> (\<exists>m \<in> M. enat k \<le> m)" (is "?L \<longleftrightarrow> ?R")
 proof cases
   assume "k = 0" then show ?thesis by (auto simp: enat_0)
 next
   assume "k \<noteq> 0"
   show ?thesis
   proof
     assume ?L
     then have "\<lbrakk>enat k \<le> (if finite M then Max M else \<infinity>); M \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>m\<in>M. enat k \<le> m"
       by (metis Max_in Sup_enat_def finite_enat_bounded linorder_linear)
     with \<open>k \<noteq> 0\<close> and \<open>?L\<close> show ?R
       unfolding Sup_enat_def
       by (cases "M={}") (auto simp add: enat_0[symmetric])
   next
     assume ?R then show ?L
       by (auto simp: enat_0 intro: complete_lattice_class.Sup_upper2)
   qed
 qed
 
 lemma enat_neq_zero_cancel_iff[simp]:
   "0 \<noteq> enat n \<longleftrightarrow> 0 \<noteq> n"
   "enat n \<noteq> 0 \<longleftrightarrow> n \<noteq> 0"
 by (auto simp: enat_0[symmetric])
 
 
 lemma natceiling_lessD: "nat(ceiling x) < n \<Longrightarrow> x < real n"
-by linarith
+  by linarith
 
 lemma le_natceiling_iff:
   fixes n :: nat and r :: real
   shows "n \<le> r \<Longrightarrow> n \<le> nat(ceiling r)"
-by linarith
+  by linarith
 
 lemma natceiling_le_iff:
   fixes n :: nat and r :: real
   shows "r \<le> n \<Longrightarrow> nat(ceiling r) \<le> n"
-by linarith
+  by linarith
 
 lemma dist_real_noabs_less:
   fixes a b c :: real assumes "dist a b < c" shows "a - b < c"
 using assms by (simp add: dist_real_def)
 
-lemma n_choose_2_nat:
-  fixes n :: nat shows "(n choose 2) = (n * (n - 1)) div 2"
-proof -
-  show ?thesis
-  proof (cases "2 \<le> n")
-    case True
-    then obtain m where "n = Suc (Suc m)"
-      by (metis add_Suc le_Suc_ex numeral_2_eq_2)
-    moreover have "(n choose 2) = (fact n div fact (n - 2)) div 2"
-      using \<open>2 \<le> n\<close> by (simp add: binomial_altdef_nat
-        div_mult2_eq[symmetric] mult.commute numeral_2_eq_2)
-    ultimately show ?thesis by (simp add: algebra_simps)
-  qed (auto simp: binomial_eq_0)
-qed
-
-lemma powr_less_one:
-  fixes x::real
-  assumes "1 < x" "y < 0"
-  shows "x powr y < 1"
-using assms less_log_iff by force
-
-lemma powr_le_one_le: "\<And>x y::real. 0 < x \<Longrightarrow> x \<le> 1 \<Longrightarrow> 1 \<le> y \<Longrightarrow> x powr y \<le> x"
-proof -
-  fix x y :: real
-  assume "0 < x" "x \<le> 1" "1 \<le> y"
-  have "x powr y = (1 / (1 / x)) powr y" using \<open>0 < x\<close> by (simp add: field_simps)
-  also have "\<dots> = 1 / (1 / x) powr y" using \<open>0 < x\<close> by (simp add: powr_divide)
-  also have "\<dots> \<le> 1 / (1 / x) powr 1" proof -
-    have "1 \<le> 1 / x" using \<open>0 < x\<close> \<open>x \<le> 1\<close> by (auto simp: field_simps)
-    then have "(1 / x) powr 1  \<le> (1 / x) powr y" using \<open>0 < x\<close>
-      using \<open>1 \<le> y\<close> by ( simp only: powr_mono)
-    then show ?thesis
-      by (metis \<open>1 \<le> 1 / x\<close> \<open>1 \<le> y\<close> neg_le_iff_le powr_minus_divide powr_mono)
-  qed
-  also have "\<dots> \<le> x" using \<open>0 < x\<close> by (auto simp: field_simps)
-  finally show "?thesis x y" .
-qed
-
-
 subsection \<open>Lists and Sets\<close>
 
 lemma list_set_tl: "x \<in> set (tl xs) \<Longrightarrow> x \<in> set xs"
-by (cases xs) auto
+  by (cases xs) auto
 
 lemma list_exhaust3:
   obtains "xs = []" | x where "xs = [x]" | x y ys where "xs = x # y # ys"
-by (metis list.exhaust)
+  by (metis list.exhaust)
 
 lemma card_Ex_subset:
   "k \<le> card M \<Longrightarrow> \<exists>N. N \<subseteq> M \<and> card N = k"
-by (induct rule: inc_induct) (auto simp: card_Suc_eq)
+  by (induct rule: inc_induct) (auto simp: card_Suc_eq)
 
 
 
 subsection \<open>Limits and eventually\<close>
 
 text \<open>
   We employ filters and the @{term eventually} predicate to deal with the
   @{term "\<exists>N. \<forall>n\<ge>N. P n"} cases. To make this more convenient, introduce
   a shorter syntax.
 \<close>
 
 abbreviation evseq :: "(nat \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>\<^sup>\<infinity>" 10) where
   "evseq P \<equiv> eventually P sequentially"
 
-lemma eventually_le_le:
-  fixes P :: "'a => ('b :: preorder)"
-  assumes "eventually (\<lambda>x. P x \<le> Q x) net"
-  assumes "eventually (\<lambda>x. Q x \<le> R  x) net"
-  shows "eventually (\<lambda>x. P x \<le> R x) net"
-using assms by eventually_elim (rule order_trans)
-
 lemma LIMSEQ_neg_powr:
   assumes s: "s < 0"
   shows "(%x. (real x) powr s) \<longlonglongrightarrow> 0"
-by (rule tendsto_neg_powr[OF assms filterlim_real_sequentially])
+  by (simp add: filterlim_real_sequentially s tendsto_neg_powr)
 
 lemma LIMSEQ_inv_powr:
   assumes "0 < c" "0 < d"
   shows "(\<lambda>n :: nat. (c / n) powr d) \<longlonglongrightarrow> 0"
 proof (rule tendsto_zero_powrI)
   from \<open>0 < c\<close> have "\<And>x. 0 < x \<Longrightarrow> 0 < c / x" by simp
   then show "\<forall>\<^sup>\<infinity>n. 0 \<le> c / real n"
     using assms(1) by auto
   show "(\<lambda>x. c / real x) \<longlonglongrightarrow> 0"
-    by (intro tendsto_divide_0[OF tendsto_const] filterlim_at_top_imp_at_infinity
-              filterlim_real_sequentially tendsto_divide_0)
-  show "0 < d" by (rule assms)
-  show "(\<lambda>x. d) \<longlonglongrightarrow> d" by auto
-qed
-
+    by (simp add: lim_const_over_n)
+qed (use assms in force)+
 
 end
diff --git a/thys/Girth_Chromatic/Ugraphs.thy b/thys/Girth_Chromatic/Ugraphs.thy
--- a/thys/Girth_Chromatic/Ugraphs.thy
+++ b/thys/Girth_Chromatic/Ugraphs.thy
@@ -1,293 +1,293 @@
 theory Ugraphs
 imports
   Girth_Chromatic_Misc
 begin
 
 section \<open>Undirected Simple Graphs\<close>
 
 text \<open>
   In this section, we define some basics of graph theory needed to formalize
   the Chromatic-Girth theorem.
 \<close>
 
 text \<open>
   For readability, we introduce synonyms for the types of vertexes, edges,
   graphs and walks.
 \<close>
 type_synonym uvert = nat
 type_synonym uedge = "nat set"
 type_synonym ugraph = "uvert set \<times> uedge set"
 type_synonym uwalk = "uvert list"
 
 abbreviation uedges :: "ugraph \<Rightarrow> uedge set" where
   "uedges G \<equiv> snd G"
 
 abbreviation uverts :: "ugraph \<Rightarrow> uvert set" where
   "uverts G \<equiv> fst G"
 
 fun mk_uedge :: "uvert \<times> uvert \<Rightarrow> uedge" where
    "mk_uedge (u,v) = {u,v}"
 
 text \<open>All edges over a set of vertexes @{term S}:\<close>
 definition "all_edges S \<equiv> mk_uedge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}"
 
 definition uwellformed :: "ugraph \<Rightarrow> bool" where
   "uwellformed G \<equiv> (\<forall>e\<in>uedges G. card e = 2 \<and> (\<forall>u \<in> e. u \<in> uverts G))"
 
 fun uwalk_edges :: "uwalk \<Rightarrow> uedge list" where
     "uwalk_edges [] = []"
   | "uwalk_edges [x] = []"
   | "uwalk_edges (x # y # ys) = {x,y} # uwalk_edges (y # ys)"
 
 definition uwalk_length :: "uwalk \<Rightarrow> nat" where
   "uwalk_length p \<equiv> length (uwalk_edges p)"
 
 definition uwalks :: "ugraph \<Rightarrow> uwalk set" where
   "uwalks G \<equiv> {p. set p \<subseteq> uverts G \<and> set (uwalk_edges p) \<subseteq> uedges G \<and> p \<noteq> []}"
 
 definition ucycles :: "ugraph \<Rightarrow> uwalk set" where
   "ucycles G \<equiv> {p. uwalk_length p \<ge> 3 \<and> p \<in> uwalks G \<and> distinct (tl p) \<and> hd p = last p}"
 
 definition remove_vertex :: "ugraph \<Rightarrow> nat \<Rightarrow> ugraph" ("_ -- _" [60,60] 60) where
   "remove_vertex G u \<equiv> (uverts G - {u}, uedges G - {A \<in> uedges G. u \<in> A})"
 
 
 subsection \<open>Basic Properties\<close>
 
 lemma uwalk_length_conv: "uwalk_length p = length p - 1"
   by (induct p rule: uwalk_edges.induct) (auto simp: uwalk_length_def)
 
 lemma all_edges_mono:
   "vs \<subseteq> ws \<Longrightarrow> all_edges vs \<subseteq> all_edges ws"
 unfolding all_edges_def by auto
 
 lemma all_edges_subset_Pow: "all_edges A \<subseteq> Pow A"
   by (auto simp: all_edges_def)
 
 lemma in_mk_uedge_img: "(a,b) \<in> A \<or> (b,a) \<in> A \<Longrightarrow> {a,b} \<in> mk_uedge ` A"
   by (auto intro: rev_image_eqI)
 
 lemma in_mk_uedge_img_iff: "{a,b} \<in> mk_uedge ` A \<longleftrightarrow> (a,b) \<in> A \<or> (b,a) \<in> A"
   by (auto simp: doubleton_eq_iff intro: rev_image_eqI)
 
 lemma distinct_edgesI:
   assumes "distinct p" shows "distinct (uwalk_edges p)"
 proof -
   from assms have "?thesis" "\<And>u. u \<notin> set p \<Longrightarrow> (\<And>v. u \<noteq> v \<Longrightarrow> {u,v} \<notin> set (uwalk_edges p))"
     by (induct p rule: uwalk_edges.induct) auto
   then show ?thesis by simp
 qed
 
 lemma finite_ucycles:
   assumes "finite (uverts G)"
   shows "finite (ucycles G)"
 proof -
   have "ucycles G \<subseteq> {xs. set xs \<subseteq> uverts G \<and> length xs \<le> Suc (card (uverts G))}"
   proof (rule, simp)
     fix p assume "p \<in> ucycles G"
     then have "distinct (tl p)" and "set p \<subseteq> uverts G"
       unfolding ucycles_def uwalks_def by auto
     moreover
     then have "set (tl p) \<subseteq> uverts G"
       by (auto simp: list_set_tl)
     with assms have "card (set (tl p)) \<le> card (uverts G)"
       by (rule card_mono)
     then have "length (p) \<le> 1 + card (uverts G)"
       using distinct_card[OF \<open>distinct (tl p)\<close>] by auto
     ultimately show "set p \<subseteq> uverts G \<and> length p \<le> Suc (card (uverts G))" by auto
   qed
   moreover
   have "finite {xs. set xs \<subseteq> uverts G \<and> length xs \<le> Suc (card (uverts G))}"
     using assms by (rule finite_lists_length_le)
   ultimately
   show ?thesis by (rule finite_subset)
 qed
 
 lemma ucycles_distinct_edges:
   assumes "c \<in> ucycles G" shows "distinct (uwalk_edges c)"
 proof -
   from assms have c_props: "distinct (tl c)" "4 \<le> length c" "hd c = last c"
     by (auto simp add: ucycles_def uwalk_length_conv)
   then have "{hd c, hd (tl c)} \<notin> set (uwalk_edges (tl c))"
   proof (induct c rule: uwalk_edges.induct)
     case (3 x y ys)
     then have "hd ys \<noteq> last ys" by (cases ys) auto
     moreover
     from 3 have "uwalk_edges (y # ys) = {y, hd ys} # uwalk_edges ys"
       by (cases ys) auto
     moreover
     { fix xs have "set (uwalk_edges xs) \<subseteq> Pow (set xs)"
         by (induct xs rule: uwalk_edges.induct) auto }
     ultimately
     show ?case using 3 by auto
   qed simp_all
   moreover
   from assms have "distinct (uwalk_edges (tl c))"
     by (intro distinct_edgesI) (simp add: ucycles_def)
   ultimately
   show ?thesis by (cases c rule: list_exhaust3) auto
 qed
 
 lemma card_left_less_pair:
   fixes A :: "('a :: linorder) set"
   assumes "finite A"
   shows "card {(a,b). a \<in> A \<and> b \<in> A \<and> a < b}
     = (card A * (card A - 1)) div 2"
 using assms
 proof (induct A)
   case (insert x A)
 
   show ?case
   proof (cases "card A")
     case (Suc n)
     have "{(a,b). a \<in> insert x A \<and> b \<in> insert x A \<and> a < b}
         = {(a,b). a \<in> A \<and> b \<in> A \<and> a < b} \<union> (\<lambda>a. if a < x then (a,x) else (x,a)) ` A"
       using \<open>x \<notin> A\<close> by (auto simp: order_less_le)
     moreover
     have "finite {(a,b). a \<in> A \<and> b \<in> A \<and> a < b}"
       using insert by (auto intro: finite_subset[of _ "A \<times> A"])
     moreover 
     have "{(a,b). a \<in> A \<and> b \<in> A \<and> a < b} \<inter> (\<lambda>a. if a < x then (a,x) else (x,a)) ` A = {}"
       using \<open>x \<notin> A\<close> by auto
     moreover have "inj_on (\<lambda>a. if a < x then (a, x) else (x, a)) A"
       by (auto intro: inj_onI split: if_split_asm)
     ultimately show ?thesis using insert Suc
       by (simp add: card_Un_disjoint card_image del: if_image_distrib)
   qed (simp add: card_eq_0_iff insert)
 qed simp
 
 lemma card_all_edges:
   assumes "finite A"
   shows "card (all_edges A) = card A choose 2"
 proof -
   have inj_on_mk_uedge: "inj_on mk_uedge {(a,b). a < b}"
     by (rule inj_onI) (auto simp: doubleton_eq_iff)
   have "all_edges A = mk_uedge ` {(a,b). a \<in> A \<and> b \<in> A \<and> a < b}" (is "?L = ?R")
     by (auto simp: all_edges_def intro!: in_mk_uedge_img)
   then have "card ?L = card ?R" by simp
   also have "\<dots> = card {(a,b). a \<in> A \<and> b \<in> A \<and> a < b}"
     using inj_on_mk_uedge by (blast intro: card_image subset_inj_on)
   also have "\<dots> = (card A * (card A - 1)) div 2"
     using card_left_less_pair using assms by simp
   also have "\<dots> = (card A choose 2)"
-    by (simp add: n_choose_2_nat)
+    by (simp add: choose_two)
   finally show ?thesis .
 qed
 
 lemma verts_Gu: "uverts (G -- u) = uverts G - {u}"
   unfolding remove_vertex_def by simp
 
 lemma edges_Gu: "uedges (G -- u) \<subseteq> uedges G"
   unfolding remove_vertex_def by auto
 
 
 subsection \<open>Girth, Independence and Vertex Colorings\<close>
 
 definition girth :: "ugraph \<Rightarrow> enat" where
   "girth G \<equiv> INF p\<in> ucycles G. enat (uwalk_length p)"
 
 definition independent_sets :: "ugraph \<Rightarrow> uvert set set" where
   "independent_sets Gr \<equiv> {vs. vs \<subseteq> uverts Gr \<and> all_edges vs \<inter> uedges Gr = {}}"
 
 definition \<alpha> :: "ugraph \<Rightarrow> enat" where
    "\<alpha> G \<equiv> SUP vs \<in> independent_sets G. enat (card vs)"
 
 definition vertex_colorings :: "ugraph \<Rightarrow> uvert set set set" where
   "vertex_colorings G \<equiv> {C. \<Union>C = uverts G \<and> (\<forall>c1\<in>C. \<forall>c2\<in>C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}) \<and>
     (\<forall>c\<in>C. c \<noteq> {} \<and> (\<forall>u \<in> c. \<forall>v \<in> c. {u,v} \<notin> uedges G))}"
 
 text \<open>The chromatic number $\chi$:\<close>
 definition chromatic_number :: "ugraph \<Rightarrow> enat" where
   "chromatic_number G \<equiv> INF c\<in> (vertex_colorings G). enat (card c)"
 
 lemma independent_sets_mono:
   "vs \<in> independent_sets G \<Longrightarrow> us \<subseteq> vs \<Longrightarrow> us \<in> independent_sets G"
   using Int_mono[OF all_edges_mono, of us vs "uedges G" "uedges G"]
   unfolding independent_sets_def by auto
 
 lemma le_\<alpha>_iff:
   assumes "0 < k"
   shows "k \<le> \<alpha> Gr \<longleftrightarrow> k \<in> card ` independent_sets Gr" (is "?L \<longleftrightarrow> ?R")
 proof
   assume ?L
   then obtain vs where "vs \<in> independent_sets Gr" and "k \<le> card vs"
     using assms unfolding \<alpha>_def enat_le_Sup_iff by auto
   moreover
   then obtain us where "us \<subseteq> vs" and "k = card us"
     using card_Ex_subset by auto
   ultimately
   have "us \<in> independent_sets Gr"  by (auto intro: independent_sets_mono)
   then show ?R using \<open>k = card us\<close> by auto
 qed (auto intro: SUP_upper simp: \<alpha>_def)
 
 lemma zero_less_\<alpha>:
   assumes "uverts G \<noteq> {}"
   shows "0 < \<alpha> G"
 proof -
   from assms obtain a where "a \<in> uverts G" by auto
   then have "0 < enat (card {a})" "{a} \<in> independent_sets G"
     by (auto simp: independent_sets_def all_edges_def)
   then show ?thesis unfolding \<alpha>_def less_SUP_iff ..
 qed
 
 lemma \<alpha>_le_card:
   assumes "finite (uverts G)"
   shows "\<alpha> G \<le> card(uverts G)"
 proof -
   { fix x assume "x \<in> independent_sets G"
     then have "x \<subseteq> uverts G" by (auto simp: independent_sets_def) }
   with assms show ?thesis unfolding \<alpha>_def
     by (intro SUP_least) (auto intro: card_mono)
 qed
 
 lemma \<alpha>_fin: "finite (uverts G) \<Longrightarrow> \<alpha> G \<noteq> \<infinity>"
   using \<alpha>_le_card[of G] by (cases "\<alpha> G") auto
 
 lemma \<alpha>_remove_le:
   shows "\<alpha> (G -- u) \<le> \<alpha> G"
 proof -
   have "independent_sets (G -- u) \<subseteq> independent_sets G" (is "?L \<subseteq> ?R")
     using all_edges_subset_Pow by (simp add: independent_sets_def remove_vertex_def) blast
   then show ?thesis unfolding \<alpha>_def
     by (rule SUP_subset_mono) simp
 qed
 
 text \<open>
   A lower bound for the chromatic number of a graph can be given in terms of
   the independence number
 \<close>
 lemma chromatic_lb:
   assumes wf_G: "uwellformed G"
     and fin_G: "finite (uverts G)"
     and neG: "uverts G \<noteq> {}"
   shows "card (uverts G) / \<alpha> G \<le> chromatic_number G"
 proof -
   from wf_G have "(\<lambda>v. {v}) ` uverts G \<in> vertex_colorings G"
     by (auto simp: vertex_colorings_def uwellformed_def)
   then have "chromatic_number G \<noteq> top"
     by (simp add: chromatic_number_def) (auto simp: top_enat_def)
   then obtain vc where vc_vc: "vc \<in> vertex_colorings G"
     and vc_size:"chromatic_number G = card vc"
     unfolding chromatic_number_def by (rule enat_in_INF)
 
   have fin_vc_elems: "\<And>c. c \<in> vc \<Longrightarrow> finite c"
     using vc_vc by (intro finite_subset[OF _ fin_G]) (auto simp: vertex_colorings_def)
 
   have sum_vc_card: "(\<Sum>c \<in> vc. card c) = card (uverts G)"
       using fin_vc_elems vc_vc unfolding vertex_colorings_def
       by (simp add: card_Union_disjoint[symmetric] pairwise_def disjnt_def)
 
   have "\<And>c. c \<in> vc \<Longrightarrow> c \<in> independent_sets G"
     using vc_vc by (auto simp: vertex_colorings_def independent_sets_def all_edges_def)
   then have "\<And>c. c \<in> vc \<Longrightarrow> card c \<le> \<alpha> G"
     using vc_vc fin_vc_elems by (subst le_\<alpha>_iff) (auto simp add: vertex_colorings_def)
   then have "(\<Sum>c\<in>vc. card c) \<le> card vc * \<alpha> G"
     using sum_bounded_above[of vc card "\<alpha> G"]
     by (simp add: of_nat_eq_enat[symmetric] of_nat_sum)
   then have "ereal_of_enat (card (uverts G)) \<le> ereal_of_enat (\<alpha> G) * ereal_of_enat (card vc)"
     by (simp add: sum_vc_card ereal_of_enat_pushout ac_simps del: ereal_of_enat_simps)
   with zero_less_\<alpha>[OF neG] \<alpha>_fin[OF fin_G] vc_size show ?thesis
     by (simp add: ereal_divide_le_pos)
 qed
 
 end
diff --git a/thys/Turans_Graph_Theorem/Turan.thy b/thys/Turans_Graph_Theorem/Turan.thy
--- a/thys/Turans_Graph_Theorem/Turan.thy
+++ b/thys/Turans_Graph_Theorem/Turan.thy
@@ -1,858 +1,858 @@
 theory Turan
   imports
     "Girth_Chromatic.Ugraphs"
     "Random_Graph_Subgraph_Threshold.Ugraph_Lemmas"
 begin
 
 section \<open>Basic facts on graphs\<close>
 
 lemma wellformed_uverts_0 :
   assumes "uwellformed G" and "uverts G = {}"
   shows "card (uedges G) = 0" using assms
   by (metis uwellformed_def card.empty ex_in_conv zero_neq_numeral)
 
 lemma finite_verts_edges :
   assumes "uwellformed G" and "finite (uverts G)"
   shows "finite (uedges G)"
 proof -
   have sub_pow: "uwellformed G \<Longrightarrow> uedges G \<subseteq> {S. S \<subseteq> uverts G}"
     by (cases G, auto simp add: uwellformed_def)
   then have "finite {S. S \<subseteq> uverts G}" using assms
     by auto
   with sub_pow assms show "finite (uedges G)"
     using finite_subset by blast
 qed
 
 lemma ugraph_max_edges :
   assumes "uwellformed G" and "card (uverts G) = n" and "finite (uverts G)"
   shows "card (uedges G) \<le> n * (n-1)/2"
   using assms wellformed_all_edges [OF assms(1)] card_all_edges [OF assms(3)] Binomial.choose_two [of "card(uverts G)"]
   by (smt (verit, del_insts) all_edges_finite card_mono dbl_simps(3) dbl_simps(5) div_times_less_eq_dividend le_divide_eq_numeral1(1) le_square nat_mult_1_right numerals(1) of_nat_1 of_nat_diff of_nat_mono of_nat_mult of_nat_numeral right_diff_distrib')
 
 lemma subgraph_verts_finite : "\<lbrakk> finite (uverts G); subgraph G' G \<rbrakk> \<Longrightarrow> finite (uverts G')"
   using rev_finite_subset subgraph_def by auto
 
 section \<open>Cliques\<close>
 
 text \<open>In this section a straightforward definition of cliques for simple, undirected graphs is introduced.
 Besides fundamental facts about cliques, also more specialized lemmata are proved in subsequent subsections.\<close>
 
 definition uclique :: "ugraph \<Rightarrow> ugraph \<Rightarrow> nat \<Rightarrow> bool" where
   "uclique C G p \<equiv> p = card (uverts C) \<and> subgraph C G \<and> C = complete (uverts C)"
 
 lemma clique_any_edge :
   assumes "uclique C G p" and "x \<in> uverts C" and "y \<in> uverts C" and "x \<noteq> y"
   shows "{x,y} \<in> uedges G"
   using assms
   apply (simp add: uclique_def complete_def all_edges_def subgraph_def)
   by (smt (verit, best) SigmaI fst_conv image_iff mem_Collect_eq mk_uedge.simps snd_conv subset_eq)
 
 lemma clique_exists : "\<exists> C p. uclique C G p \<and> p \<le> card (uverts G)"
   using bex_imageD card.empty emptyE gr_implies_not0 le_neq_implies_less
   by (auto simp add: uclique_def complete_def subgraph_def all_edges_def)
 
 lemma clique_exists1 :
   assumes "uverts G \<noteq> {}" and "finite (uverts G)"
   shows "\<exists> C p. uclique C G p \<and> 0 < p \<and>  p \<le> card (uverts G)"
 proof -
   obtain x where x: "x \<in> uverts G"
     using assms
     by auto
   show ?thesis
     apply (rule exI [of _ "({x},{})"], rule exI [of _ 1])
     using x assms(2)
     by (simp add: uclique_def subgraph_def complete_def all_edges_def Suc_leI assms(1) card_gt_0_iff)
 qed
 
 lemma clique_max_size : "uclique C G p \<Longrightarrow> finite (uverts G) \<Longrightarrow>  p \<le> card (uverts G)"
   by (auto simp add: uclique_def subgraph_def Finite_Set.card_mono)
 
 lemma clique_exists_gt0 :
   assumes "finite (uverts G)" "card (uverts G) > 0"
   shows "\<exists> C p. uclique C G p \<and> p \<le> card (uverts G) \<and> (\<forall>C q. uclique C G q \<longrightarrow> q \<le> p)"
 proof -
   have 1: "finite (uverts G) \<Longrightarrow> finite {p. \<exists>C. uclique C G p}"
     using clique_max_size
     by (smt (verit, best) finite_nat_set_iff_bounded_le mem_Collect_eq)
   have 2: "\<And>A::nat set. finite A \<Longrightarrow> \<exists>x. x\<in>A \<Longrightarrow> \<exists>x\<in>A.\<forall>y\<in>A. y \<le> x"
     using Max_ge Max_in by blast
   have "\<exists>C p. uclique C G p \<and> (\<forall>C q. uclique C G q \<longrightarrow> q \<le> p)"
     using 2 [OF 1 [OF \<open>finite (uverts G)\<close>]] clique_exists [of G]
     by (smt (z3) mem_Collect_eq)
   then show ?thesis
     using \<open>finite (uverts G)\<close> clique_max_size
     by blast
 qed
 
 text \<open>If there exists a $(p+1)$-clique @{term C} in a graph @{term G}
       then we can obtain a $p$-clique in @{term G} by removing an arbitrary vertex from @{term C}\<close>
 
 lemma clique_size_jumpfree :
   assumes "finite (uverts G)" and "uwellformed G"
     and "uclique C G (p+1)"
   shows "\<exists>C'. uclique C' G p"
 proof -
   have "card(uverts G) > p"
     using assms by (simp add: uclique_def subgraph_def card_mono less_eq_Suc_le)
   obtain x where x: "x \<in> uverts C"
     using assms by (fastforce simp add: uclique_def)
   have "mk_uedge ` {uv \<in> uverts C \<times> uverts C. fst uv \<noteq> snd uv} - {A \<in> uedges C. x \<in> A} =
     mk_uedge ` {uv \<in> (uverts C - {x}) \<times> (uverts C - {x}). fst uv \<noteq> snd uv}"
   proof -
     have "\<And>y. y \<in> mk_uedge ` {uv \<in> uverts C \<times> uverts C. fst uv \<noteq> snd uv} - {A \<in> uedges C. x \<in> A} \<Longrightarrow>
           y \<in> mk_uedge ` {uv \<in> (uverts C - {x}) \<times> (uverts C - {x}). fst uv \<noteq> snd uv}"
       using assms(3)
       apply (simp add: uclique_def complete_def all_edges_def)
       by (smt (z3) DiffI SigmaE SigmaI image_iff insertCI mem_Collect_eq mk_uedge.simps singleton_iff snd_conv)
     moreover have "\<And>y. y \<in> mk_uedge ` {uv \<in> (uverts C - {x}) \<times> (uverts C - {x}). fst uv \<noteq> snd uv}
                   \<Longrightarrow> y \<in> mk_uedge ` {uv \<in> uverts C \<times> uverts C. fst uv \<noteq> snd uv} - {A \<in> uedges C. x \<in> A}"
       apply (simp add: uclique_def complete_def all_edges_def)
       by (smt (z3) DiffE SigmaE SigmaI image_iff insert_iff mem_Collect_eq mk_uedge.simps singleton_iff)
     ultimately show ?thesis
       by blast
   qed
   then have 1: "(uverts C - {x}, uedges C - {A \<in> uedges C. x \<in> A}) = Ugraph_Lemmas.complete (uverts C - {x})"
     using assms(3)
     apply (simp add: uclique_def complete_def all_edges_def)
     by (metis (no_types, lifting) snd_eqD)
   show ?thesis
     apply (rule exI [of _ "C -- x"])
     using assms x
     apply (simp add: uclique_def remove_vertex_def subgraph_def)
     apply (simp add: 1)
     by (auto simp add: complete_def all_edges_def)
 qed
 
 text \<open>The next lemma generalises the lemma @{thm [source] clique_size_jumpfree} to a proof of
  the existence of a clique of any size smaller than the size of the original clique.\<close>
 
 lemma clique_size_decr :
   assumes "finite (uverts G)" and "uwellformed G"
     and "uclique C G p"
   shows "q \<le> p \<Longrightarrow> \<exists>C. uclique C G q" using assms
 proof (induction q rule: measure_induct [of "\<lambda>x. p - x"])
   case (1 x)
   then show ?case
   proof (cases "x = p")
     case True
     then show ?thesis
       using \<open>uclique C G p\<close>
       by blast
   next
     case False
     with 1(2) have "x < p"
       by auto
     from \<open>x < p\<close> have "p - Suc x < p - x"
       by auto
     then show ?thesis
       using 1(1) assms(1,2,3) \<open>x < p\<close>
       using clique_size_jumpfree [OF \<open>finite (uverts G)\<close> \<open>uwellformed G\<close> _]
       by (metis "1.prems"(4) add.commute linorder_not_le not_less_eq plus_1_eq_Suc)
   qed
 qed
 
 text \<open>With this lemma we can easily derive by contradiction that
       if there is no $p$-clique then there cannot exist a clique of a size greater than @{term p}\<close>
 
 corollary clique_size_neg_max :
   assumes "finite (uverts G)" and "uwellformed G"
     and "\<not>(\<exists>C. uclique C G p)"
   shows "\<forall>C q. uclique C G q \<longrightarrow> q < p"
 proof (rule ccontr)
   assume 1: "\<not> (\<forall>C q. uclique C G q \<longrightarrow> q < p)"
   show False
   proof -
     obtain C q where C: "uclique C G q"
       and q: "q \<ge> p"
       using 1 linorder_not_less
       by blast
     show ?thesis
       using assms(3) q clique_size_decr [OF \<open>finite (uverts G)\<close> \<open>uwellformed G\<close> C ]
       using order_less_imp_le by blast
   qed
 qed
 
 corollary clique_complete :
   assumes "finite V" and "x \<le> card V"
   shows "\<exists>C. uclique C (complete V) x"
 proof -
   have "uclique (complete V) (complete V) (card V)"
     by (simp add: uclique_def complete_def subgraph_def)
   then show ?thesis
     using clique_size_decr [OF _ complete_wellformed [of V] _ assms(2)] assms(1)
     by (simp add: complete_def)
 qed
 
 lemma subgraph_clique :
   assumes "uwellformed G" "subgraph C G" "C = complete (uverts C)"
   shows "{e \<in> uedges G. e \<subseteq> uverts C} = uedges C"
 proof -
   from assms complete_wellformed [of "uverts C"] have "uedges C \<subseteq> {e \<in> uedges G. e \<subseteq> uverts C}"
     by (auto simp add: subgraph_def uwellformed_def)
   moreover from assms(1) complete_wellformed [of "uverts C"] have "{e \<in> uedges G. e \<subseteq> uverts C} \<subseteq> uedges C"
     apply (simp add: subgraph_def uwellformed_def complete_def card_2_iff all_edges_def)
     using assms(3)[unfolded complete_def all_edges_def] in_mk_uedge_img 
     by (smt (verit, ccfv_threshold) SigmaI fst_conv insert_subset mem_Collect_eq snd_conv subsetI)
   ultimately show ?thesis
     by auto
 qed
 
 text \<open>Next, we prove that in a graph @{term G} with a $p$-clique @{term C} and some vertex @{term v} outside of this clique,
 there exists a $(p+1)$-clique in @{term G} if @{term v} is connected to all nodes in @{term C}.
 The next lemma is an abstracted version that does not explicitly mention cliques:
 If a vertex @{term n} has as many edges to a set of nodes @{term N} as there are nodes in @{term N}
 then @{term n} is connected to all vertices in @{term N}.\<close>
 
 lemma card_edges_nodes_all_edges :
   fixes G :: "ugraph" and  N :: "nat set" and E :: "nat set set" and n :: nat
   assumes "uwellformed G"
     and "finite N"
     and "N \<subseteq> uverts G" and "E \<subseteq> uedges G"
     and "n \<in> uverts G" and "n \<notin> N"
     and "\<forall>e \<in> E. \<exists>x \<in> N. {n,x} = e"
     and "card E = card N"
   shows "\<forall>x \<in> N. {n,x} \<in> E"
 proof (rule ccontr)
   assume "\<not>(\<forall>x \<in> N. {n,x} \<in> E)"
   show False
   proof -
     obtain x where x: "x \<in> N" and e: "{n,x} \<notin> E"
       using \<open>\<not>(\<forall>x \<in> N. {n,x} \<in> E)\<close>
       by auto
     have "E \<subseteq> (\<lambda>y. {n,y}) ` (N - {x})"
       using Set.image_diff_subset \<open>\<forall>e \<in> E. \<exists>x \<in> N. {n,x} = e\<close> x e
       by auto
     then show ?thesis
       using \<open>finite N\<close> \<open>card E = card N\<close> x
       using surj_card_le [of "N - {x}" E "(\<lambda>y. {n,y})"]
       by (simp, metis card_gt_0_iff diff_less emptyE lessI linorder_not_le)
   qed
 qed
 
 subsection \<open>Partitioning edges along a clique\<close>
 
 text \<open>Tur\'{a}n's proof partitions the edges of a graph into three partitions for a $(p-1)$-clique @{term C}:
 All edges within @{term C}, all edges outside of @{term C}, and all edges between a vertex in @{term C} and a
 vertex not in @{term C}.
 
 We prove a generalized lemma that partitions the edges along some arbitrary set of vertices
 which does not necessarily need to induce a clique.
 Furthermore, in Tur\'{a}n's graph theorem we only argue about the cardinality of the partitions
 so that we restrict this proof to showing that
 the sum of the cardinalities of the partitions is equal to number of all edges.\<close>
 
 lemma graph_partition_edges_card :
   assumes "finite (uverts G)" and "uwellformed G" and "A \<subseteq> (uverts G)"
   shows "card (uedges G) = card {e \<in> uedges G. e \<subseteq> A} + card {e \<in> uedges G.  e \<subseteq> uverts G - A} + card {e \<in> uedges G. e \<inter> A \<noteq> {} \<and> e \<inter> (uverts G - A) \<noteq> {}}"
   using assms
 proof -
   have "uedges G = {e \<in> uedges G. e \<subseteq> A} \<union> {e \<in> uedges G.  e \<subseteq> (uverts G) - A} \<union> {e \<in> uedges G. e \<inter> A \<noteq> {} \<and> e \<inter> ((uverts G) - A) \<noteq> {}}"
     using assms uwellformed_def
     by blast
   moreover have "{e \<in> uedges G. e \<subseteq> A} \<inter> {e \<in> uedges G.  e \<subseteq> uverts G - A} = {}"
     using assms uwellformed_def
     by (smt (verit, ccfv_SIG) Diff_disjoint Int_subset_iff card.empty disjoint_iff mem_Collect_eq nat.simps(3) nat_1_add_1 plus_1_eq_Suc prod.sel(2) subset_empty)
   moreover have "({e \<in> uedges G. e \<subseteq> A} \<union> {e \<in> uedges G.  e \<subseteq> uverts G - A}) \<inter> {e \<in> uedges G. e \<inter> A \<noteq> {} \<and> e \<inter> (uverts G - A) \<noteq> {}} = {}"
     by blast
   moreover have "finite {e \<in> uedges G. e \<subseteq> A}" using assms
     by (simp add: finite_subset)
   moreover have "finite {e \<in> uedges G.  e \<subseteq> uverts G - A}" using assms
     by (simp add: finite_subset)
   moreover have "finite {e \<in> uedges G. e \<inter> A \<noteq> {} \<and> e \<inter> (uverts G - A) \<noteq> {}}"
     using assms finite_verts_edges
     by auto
   ultimately show ?thesis
     using assms Finite_Set.card_Un_disjoint
     by (smt (verit, best) finite_UnI)
 qed
 
 text \<open>Now, we turn to the problem of calculating the cardinalities of these partitions
 when they are induced by the biggest clique in the graph.
 
 First, we consider the number of edges in a $p$-clique.\<close>
 
 lemma clique_edges_inside :
   assumes G1: "uwellformed G" and G2: "finite (uverts G)"
     and p: "p \<le> card (uverts G)" and n: "n = card(uverts G)"
     and C: "uclique C G p"
   shows "card {e \<in> uedges G. e \<subseteq> uverts C} = p * (p-1) / 2"
 proof -
   have "2 dvd (card (uverts C) * (p - 1))"
     using C uclique_def
     by auto
   have "2 = real 2"
     by simp
   then show ?thesis
     using C uclique_def [of C G p] complete_def [of "uverts C"]
     using subgraph_clique [OF G1, of C] subgraph_verts_finite [OF assms(2), of C]
     using Real.real_of_nat_div [OF \<open>2 dvd (card (uverts C) * (p - 1))\<close>] Binomial.choose_two [of " card (uverts G)"]
-    by (smt (verit, del_insts) One_nat_def approximation_preproc_nat(5) card_all_edges diff_self_eq_0 eq_imp_le left_diff_distrib' left_diff_distrib' linorder_not_less mult_le_mono2 n_choose_2_nat not_gr0 not_less_eq_eq of_nat_1 of_nat_diff snd_eqD)
+    by (smt (verit, del_insts) One_nat_def approximation_preproc_nat(5) card_all_edges diff_self_eq_0 eq_imp_le left_diff_distrib' left_diff_distrib' linorder_not_less mult_le_mono2 choose_two not_gr0 not_less_eq_eq of_nat_1 of_nat_diff snd_eqD)
 qed
 
 text \<open>Next, we turn to the number of edges that connect a node inside of the biggest clique with
 a node outside of said clique. For that we start by calculating a bound for the number of
 edges from one single node outside of the clique into the clique.\<close>
 
 lemma clique_edges_inside_to_node_outside :
   assumes "uwellformed G" and "finite (uverts G)"
   assumes "0 < p" and "p \<le> card (uverts G)"
   assumes "uclique C G p" and "(\<forall>C p'. uclique C G p' \<longrightarrow> p' \<le> p)"
   assumes y: "y \<in> uverts G - uverts C"
   shows "card {{x,y}| x. x \<in> uverts C \<and> {x,y} \<in> uedges G} \<le> p - 1"
 proof (rule ccontr)
   txt \<open>For effective proof automation we use a local function definition to compute this
        set of edges into the clique from any node @{term y}:\<close>
   define S where "S \<equiv> \<lambda>y. {{x,y}| x. x \<in> uverts C \<and> {x,y} \<in> uedges G}"
   assume "\<not> card {{x, y} |x. x \<in> uverts C \<and> {x, y} \<in> uedges G} \<le> p - 1"
   then have Sy: "card (S y) > p - 1"
     using S_def y by auto
   have "uclique ({y} \<union> (uverts C),S y \<union> uedges C) G (Suc p)"
   proof -
     have "card ({y} \<union> uverts C) = Suc p"
       using assms(3,5,7) uclique_def
       by (metis DiffD2 card_gt_0_iff card_insert_disjoint insert_is_Un)
     moreover have "subgraph ({y} \<union> uverts C, (S y) \<union> uedges C) G"
       using assms(5,7)
       by (auto simp add: uclique_def subgraph_def S_def)
     moreover have "({y} \<union> (uverts C),(S y) \<union> uedges C) = complete ({y} \<union> (uverts C))"
     proof -
       have "(S y) \<union> uedges C \<subseteq> all_edges ({y} \<union> (uverts C))"
         using y assms(5) S_def all_edges_def uclique_def complete_def
         by (simp, smt (z3) SigmaE SigmaI fst_conv image_iff in_mk_uedge_img insertCI mem_Collect_eq snd_conv subsetI)
       moreover have "all_edges ({y} \<union> (uverts C)) \<subseteq> (S y) \<union> uedges C"
       proof -
         have "\<forall>x\<in>uverts C. {y, x} \<in> S y"
         proof -
           have "card (S y) = card (uverts C)"
             using Sy assms(2,3,5,7) S_def uclique_def card_gt_0_iff
             using Finite_Set.surj_card_le [of "uverts C" "S y" "\<lambda>x. {x, y}"]
             by (smt (verit, del_insts) Suc_leI Suc_pred' image_iff le_antisym mem_Collect_eq subsetI)
           then show ?thesis
             using card_edges_nodes_all_edges [OF assms(1), of "uverts C" "S y" y] assms(1,2,5,7) S_def uclique_def
             by (smt (verit, ccfv_threshold) DiffE insert_commute mem_Collect_eq subgraph_def subgraph_verts_finite subsetI)
         qed
         then show ?thesis
           using assms(5) all_edges_def S_def uclique_def complete_def mk_uedge.simps in_mk_uedge_img
           by (smt (z3) insert_commute SigmaI fst_conv mem_Collect_eq snd_conv SigmaE UnCI image_iff insert_iff insert_is_Un subsetI)
       qed
       ultimately show ?thesis
         by (auto simp add: complete_def)
     qed
     ultimately show ?thesis
       by (simp add: uclique_def complete_def)
   qed
   then show False
     using assms(6)
     by fastforce
 qed
 
 text \<open>Now, that we have this upper bound for the number of edges from a single vertex into the largest clique
       we can calculate the upper bound for all such vertices and edges:\<close>
 
 lemma clique_edges_inside_to_outside :
   assumes G1: "uwellformed G" and G2: "finite (uverts G)"
     and p0: "0 < p" and pn: "p \<le> card (uverts G)" and "card(uverts G) = n"
     and C: "uclique C G p" and C_max: "(\<forall>C p'. uclique C G p' \<longrightarrow> p' \<le> p)"
   shows "card {e \<in> uedges G. e \<inter> uverts C \<noteq> {} \<and> e \<inter> (uverts G - uverts C) \<noteq> {}} \<le> (p - 1) * (n - p)"
 proof -
   define S where "S \<equiv> \<lambda>y. {{x,y}| x. x \<in> uverts C \<and> {x,y} \<in> uedges G}"
   have "card (uverts G - uverts C) = n - p"
     using pn C \<open>card(uverts G) = n\<close> G2
     apply (simp add: uclique_def)
     by (meson card_Diff_subset subgraph_def subgraph_verts_finite)
   moreover have "{e \<in> uedges G. e \<inter> uverts C \<noteq> {} \<and> e \<inter> (uverts G - uverts C) \<noteq> {}} = {{x,y}| x y. x \<in> uverts C \<and> y \<in> (uverts G - uverts C) \<and> {x,y} \<in> uedges G}"
   proof -
     have "e \<in> {e \<in> uedges G. e \<inter> uverts C \<noteq> {} \<and> e \<inter> (uverts G - uverts C) \<noteq> {}}
           \<Longrightarrow> \<exists>x y. e = {x,y} \<and> x \<in> uverts C \<and> y \<in> uverts G - uverts C" for e
       using G1
       apply (simp add: uwellformed_def)
       by (smt (z3) DiffD2 card_2_iff disjoint_iff_not_equal insert_Diff insert_Diff_if insert_iff)
     then show ?thesis
       by auto
   qed
   moreover have "card {{x,y}| x y. x \<in> uverts C \<and> y \<in> (uverts G - uverts C) \<and> {x,y} \<in> uedges G} \<le> card (uverts G - uverts C) * (p-1)"
   proof -
     have "card {{x,y}| x y. x \<in> uverts C \<and> y \<in> (uverts G - uverts C) \<and> {x,y} \<in> uedges G}
            \<le> (\<Sum>y \<in> (uverts G - uverts C). card (S y))"
     proof -
       have "finite (uverts G - uverts C)"
         using \<open>finite (uverts G)\<close> by auto
       have "{{x,y}| x y. x \<in> uverts C \<and> y \<in> (uverts G - uverts C) \<and> {x,y} \<in> uedges G}
            = (\<Union>y \<in> (uverts G - uverts C). {{x,y}| x. x \<in> uverts C \<and> {x,y} \<in> uedges G})"
         by auto
       then show ?thesis
         using Groups_Big.card_UN_le [OF \<open>finite (uverts G - uverts C)\<close>,
             of "\<lambda>y. {{x, y} |x. x \<in> uverts C \<and> {x, y} \<in> uedges G}"]
         using S_def
         by auto
     qed
     moreover have "(\<Sum>y\<in>uverts G - uverts C. card (S y)) \<le> card (uverts G - uverts C) * (p-1)"
     proof -
       have "card (S y) \<le> p - 1" if y: "y \<in> uverts G - uverts C" for y
         using clique_edges_inside_to_node_outside [OF assms(1,2,3,4) C C_max y] S_def y
         by simp
       then show ?thesis
         by (metis id_apply of_nat_eq_id sum_bounded_above)
     qed
     ultimately show ?thesis
       using order_trans
       by blast
   qed
   ultimately show ?thesis
     by (smt (verit, ccfv_SIG) mult.commute)
 qed
 
 text \<open>Lastly, we need to argue about the number of edges which are located entirely outside of
 the greatest clique. Note that this is in the inductive step case in the overarching proof
 of  Tur\'{a}n's graph theorem. That is why we have access to the inductive hypothesis as an
 assumption in the following lemma:\<close>
 
 lemma clique_edges_outside :
   assumes "uwellformed G" and "finite (uverts G)"
     and p2: "2 \<le> p" and pn: "p \<le> card (uverts G)" and n: "n = card(uverts G)"
     and C: "uclique C G (p-1)" and C_max: "(\<forall>C q. uclique C G q \<longrightarrow> q \<le> p-1)"
     and IH: "\<And>G y. y < n \<Longrightarrow> finite (uverts G) \<Longrightarrow> uwellformed G \<Longrightarrow> \<forall>C p'. uclique C G p' \<longrightarrow> p' < p
               \<Longrightarrow> 2 \<le> p \<Longrightarrow> card (uverts G) = y \<Longrightarrow> real (card (uedges G)) \<le> (1 - 1 / real (p - 1)) * real (y\<^sup>2) / 2"
   shows "card {e \<in> uedges G. e \<subseteq> uverts G - uverts C} \<le> (1 - 1 / (p-1)) * (n - p + 1) ^ 2 / 2"
 proof -
   have "n - card (uverts C) < n"
     using C pn p2 n
     by (metis Suc_pred' diff_less less_2_cases_iff linorder_not_less not_gr0 uclique_def)
   have GC1: "finite (uverts (uverts G - uverts C, {e \<in> uedges G. e \<subseteq> uverts G - uverts C}))"
     using assms(2)
     by simp
   have GC2: "uwellformed (uverts G - uverts C, {e \<in> uedges G. e \<subseteq> uverts G - uverts C})"
     using assms(1)
     by (auto simp add: uwellformed_def)
   have GC3: "\<forall>C' p'. uclique C' (uverts G - uverts C, {e \<in> uedges G. e \<subseteq> uverts G - uverts C}) p' \<longrightarrow> p' < p"
   proof (rule ccontr)
     assume "\<not>(\<forall>C' p'. uclique C' (uverts G - uverts C, {e \<in> uedges G. e \<subseteq> uverts G - uverts C}) p' \<longrightarrow> p' < p)"
     then obtain C' p' where C': "uclique C' (uverts G - uverts C, {e \<in> uedges G. e \<subseteq> uverts G - uverts C}) p'" and p': "p' \<ge> p"
       by auto
     then have "uclique C' G p'"
       using uclique_def subgraph_def
       by auto
     then show False
       using p' p2 C_max
       by fastforce
   qed
   have GC4: "card (uverts (uverts G - uverts C,{e \<in> uedges G. e \<subseteq> uverts G - uverts C})) = n - card (uverts C)"
     using C n assms(2) uclique_def subgraph_def
     by (simp, meson card_Diff_subset infinite_super)
   show ?thesis
     using C GC3 IH [OF \<open>n - card (uverts C) < n\<close> GC1 GC2 GC3 \<open>2 \<le> p\<close> GC4] assms(2) n uclique_def
     by (simp, smt (verit, best) C One_nat_def Suc_1 Suc_leD clique_max_size of_nat_1 of_nat_diff p2)
 qed
 
 subsection \<open>Extending the size of the biggest clique\<close> text_raw \<open>\label{sec:extend_clique}\<close>
 
 text \<open>In this section, we want to prove that we can add edges to a graph so that we augment the biggest clique
 to some greater clique with a specific number of vertices. For that, we need the following lemma:
 When too many edges have been added to a graph so that there exists a $(p+1)$-clique
 then we can remove at least one of the added edges while also retaining a p-clique\<close>
 
 lemma clique_union_size_decr :
   assumes "finite (uverts G)" and "uwellformed (uverts G, uedges G \<union> E)"
     and "uclique C (uverts G, uedges G \<union> E) (p+1)"
     and "card E \<ge> 1"
   shows "\<exists>C' E'. card E' < card E \<and> uclique C' (uverts G, uedges G \<union> E') p \<and> uwellformed (uverts G, uedges G \<union> E')"
 proof (cases "\<exists>x \<in> uverts C. \<exists>e \<in> E. x \<in> e")
   case True
   then obtain x where x1: "x \<in> uverts C" and x2: "\<exists>e \<in> E. x \<in> e"
     by auto
   show ?thesis
   proof (rule exI [of _ "C -- x"], rule exI [of _ "{e \<in> E. x \<notin> e}"])
     have "card {e \<in> E. x \<notin> e} < card E"
       using x2 assms(4)
       by (smt (verit) One_nat_def card.infinite diff_is_0_eq mem_Collect_eq minus_nat.diff_0 not_less_eq psubset_card_mono psubset_eq subset_eq)
     moreover have "uclique (C -- x) (uverts G, uedges G \<union> {e \<in> E. x \<notin> e}) p"
     proof -
       have "p = card (uverts (C -- x))"
         using x1 assms(3)
         by (auto simp add: uclique_def remove_vertex_def)
       moreover have "subgraph (C -- x) (uverts G, uedges G \<union> {e \<in> E. x \<notin> e})"
         using assms(3)
         by (auto simp add: uclique_def subgraph_def remove_vertex_def)
       moreover have "C -- x = Ugraph_Lemmas.complete (uverts (C -- x))"
       proof -
         have 1: "\<And>y. y \<in> mk_uedge ` {uv \<in> uverts C \<times> uverts C. fst uv \<noteq> snd uv} - {A \<in> uedges C. x \<in> A} \<Longrightarrow>
             y \<in> mk_uedge ` {uv \<in> (uverts C - {x}) \<times> (uverts C - {x}). fst uv \<noteq> snd uv}"
           by (smt (z3) DiffE DiffI SigmaE SigmaI Ugraph_Lemmas.complete_def all_edges_def assms(3) empty_iff image_iff insert_iff mem_Collect_eq mk_uedge.simps snd_conv uclique_def)
         have 2: "\<And>y. y \<in> mk_uedge ` {uv \<in> (uverts C - {x}) \<times> (uverts C - {x}). fst uv \<noteq> snd uv} \<Longrightarrow>
             y \<in> mk_uedge ` {uv \<in> uverts C \<times> uverts C. fst uv \<noteq> snd uv} - {A \<in> uedges C. x \<in> A}"
           by (smt (z3) DiffE DiffI SigmaE SigmaI image_iff insert_iff mem_Collect_eq mk_uedge.simps singleton_iff)
         show ?thesis
           using assms(3)
           apply (simp add: remove_vertex_def complete_def all_edges_def uclique_def)
           using 1 2
           by (smt (verit, ccfv_SIG) split_pairs subset_antisym subset_eq)
       qed
       ultimately show ?thesis
         by (simp add: uclique_def)
     qed
     moreover have "uwellformed (uverts G, uedges G \<union> {e \<in> E. x \<notin> e})"
       using assms(2)
       by (auto simp add: uwellformed_def)
     ultimately show "card {e \<in> E. x \<notin> e} < card E \<and>
     uclique (C -- x) (uverts G, uedges G \<union> {e \<in> E. x \<notin> e}) p \<and>
     uwellformed (uverts G, uedges G \<union> {e \<in> E. x \<notin> e})"
       by auto
   qed
 next
   case False
   then have "\<And>x. x \<in> uedges C \<Longrightarrow> x \<notin> E"
     using assms(2)
     by (metis assms(3) card_2_iff' complete_wellformed uclique_def uwellformed_def)
   then have "uclique C G (p+1)"
     using assms(3)
     by (auto simp add: uclique_def subgraph_def uwellformed_def)
   show ?thesis
     using assms(2,4) clique_size_jumpfree [OF assms(1) _ \<open>uclique C G (p+1)\<close>]
     apply (simp add: uwellformed_def)
     by (metis Suc_le_eq UnCI Un_empty_right card.empty prod.exhaust_sel)
 qed
 
 text \<open>We use this preceding lemma to prove the next result. In this lemma we assume that we have
 added too many edges. The goal is then to remove some of the new edges appropriately so
 that it is indeed guaranteed that there is no bigger clique.
 
 Two proofs of this lemma will be described in the following.
 Both fundamentally come down to the same core idea:
 In essence, both proofs apply the well-ordering principle.
 In the first proof we do so immediately by obtaining the minimum of a set:\<close>
 
 lemma clique_union_make_greatest :
   fixes p n :: nat
   assumes "finite (uverts G)" and "uwellformed G"
     and "uwellformed (uverts G, uedges G \<union> E)" and "card(uverts G) \<ge> p"
     and "uclique C (uverts G, uedges G \<union> E) p"
     and "\<forall>C' q'. uclique C' G q' \<longrightarrow> q' < p" and "1 \<le> card E"
   shows "\<exists>C' E'. uwellformed (uverts G, uedges G \<union> E')
         \<and> (uclique C' (uverts G, uedges G \<union> E') p)
         \<and> (\<forall>C'' q'. uclique C'' (uverts G, uedges G \<union> E') q' \<longrightarrow> q' \<le> p)"
   using assms
 proof  (induction "card E" arbitrary: C E rule: less_induct)
   case (less E)
   then show ?case
   proof (cases "\<exists>A. uclique A (uverts G, uedges G \<union> E) (p+1)")
     case True
     then obtain A where A: "uclique A (uverts G, uedges G \<union> E) (p+1)"
       by auto
     obtain C' E' where E'1: "card E' < card E"
       and E'2: "uclique C' (uverts G, uedges G \<union> E') p"
       and E'3: "uwellformed (uverts G, uedges G \<union> E')"
       and E'4: "1 \<le> card E'"
       using less(7)
       using clique_union_size_decr [OF assms(1) \<open>uwellformed (uverts G, uedges G \<union> E)\<close> A less(8)]
       by (metis One_nat_def Suc_le_eq Un_empty_right card_gt_0_iff finite_Un finite_verts_edges fst_conv less.prems(1) less_not_refl prod.collapse snd_conv)
     show ?thesis
       using less(1) [OF E'1 assms(1,2) E'3 less(5) E'2 less(7) E'4]
       using E'1 less(8)
       by (meson less_or_eq_imp_le order_le_less_trans)
   next
     case False
     show ?thesis
       apply (rule exI [of _ C], rule exI [of _ E])
       using clique_size_neg_max [OF _ less(4) False]
       using less(2,4,6)
       by fastforce
   qed
 qed
 
 text \<open>In this second, alternative proof the well-ordering principle is used through complete induction.\<close>
 
 lemma clique_union_make_greatest_alt :
   fixes p n :: nat
   assumes "finite (uverts G)" and "uwellformed G"
     and "uwellformed (uverts G, uedges G \<union> E)" and "card(uverts G) \<ge> p"
     and "uclique C (uverts G, uedges G \<union> E) p"
     and "\<forall>C' q'. uclique C' G q' \<longrightarrow> q' < p" and "1 \<le> card E"
   shows "\<exists>C' E'. uwellformed (uverts G, uedges G \<union> E')
         \<and> (uclique C' (uverts G, uedges G \<union> E') p)
         \<and> (\<forall>C'' q'. uclique C'' (uverts G, uedges G \<union> E') q' \<longrightarrow> q' \<le> p)"
 proof -
   define P where "P \<equiv> \<lambda>E. uwellformed (uverts G, uedges G \<union> E) \<and> (\<exists>C. uclique C (uverts G, uedges G \<union> E) p)"
   have "finite {y. \<exists>E. P E \<and> card E = y}"
   proof -
     have "\<And>E. P E \<Longrightarrow> E \<subseteq> Pow (uverts G)"
       by (auto simp add: P_def uwellformed_def)
     then have "finite {E. P E}"
       using assms(1)
       by (metis Collect_mono Pow_def finite_Pow_iff rev_finite_subset)
     then show ?thesis
       by simp
   qed
   obtain F where F1: "P F"
     and F2: "card F = Min {y. \<exists>E. P E \<and> card E = y}"
     and F3: "card F > 0"
     using assms(1,3,4,5,6) Min_in \<open>finite {y. \<exists>E. P E \<and> card E = y}\<close> P_def CollectD Collect_empty_eq
     by (smt (verit, ccfv_threshold) Un_empty_right card_gt_0_iff finite_Un finite_verts_edges fst_conv le_refl linorder_not_le prod.collapse snd_conv)
   have "p > 0"
     using assms(6) clique_exists bot_nat_0.not_eq_extremum
     by blast
   then show ?thesis
   proof (cases "\<exists>C. uclique C (uverts G, uedges G \<union> F) (p + 1)")
     case True
     then obtain F' where F'1 : "P F'" and F'2: "card F' < card F"
       using F1 F2 F3 clique_union_size_decr [OF assms(1), of F _ p] P_def
       by (smt (verit) One_nat_def Suc_eq_plus1 Suc_leI add_2_eq_Suc' assms(1) clique_size_jumpfree fst_conv)
     then show ?thesis
       using F2 \<open>finite {y. \<exists>F. P F \<and> card F = y}\<close> Min_gr_iff
       by fastforce
   next
     case False
     then show ?thesis
       using clique_size_neg_max [OF _ _ False]
       using assms(1) F1 P_def
       by (smt (verit, ccfv_SIG) Suc_eq_plus1 Suc_leI fst_conv linorder_not_le)
   qed
 qed
 
 text \<open>Finally, with this lemma we can turn to this section's main challenge of increasing the
 greatest clique size of a graph by adding edges.\<close>
 
 lemma clique_add_edges_max :
   fixes p :: nat
   assumes "finite (uverts G)"
     and "uwellformed G" and "card(uverts G) > p"
     and "\<exists>C. uclique C G p" and "(\<forall>C q'. uclique C G q' \<longrightarrow> q' \<le> p)"
     and "q \<le> card(uverts G)" and "p \<le> q"
   shows "\<exists>E. uwellformed (uverts G, uedges G \<union> E) \<and> (\<exists>C. uclique C (uverts G, uedges G \<union> E) q)
         \<and> (\<forall>C q'. uclique C (uverts G, uedges G \<union> E) q' \<longrightarrow> q' \<le> q)"
 proof (cases "p < q")
   case True
   then show ?thesis
   proof -
     have "\<exists>E. uwellformed (uverts G, uedges G \<union> E) \<and> (\<exists>C. uclique C (uverts G, uedges G \<union> E) q) \<and> card E \<ge> 1"
       apply (rule exI [of _ "all_edges (uverts G)"])
       using Set.Un_absorb1 [OF wellformed_all_edges [OF assms(2)]]
       using complete_wellformed [of "uverts G"] clique_complete [OF assms(1,6)]
       using all_edges_def assms(1,5)
       apply (simp add: complete_def)
       by (metis Suc_leI True Un_empty_right all_edges_finite card_gt_0_iff linorder_not_less prod.collapse)
     then obtain E C where E1: "uwellformed (uverts G, uedges G \<union> E)"
       and E2: "uclique C (uverts G, uedges G \<union> E) q"
       and E3: "card E \<ge> 1"
       by auto
     show ?thesis
       using clique_union_make_greatest [OF assms(1,2) E1 assms(6) E2 _ E3] assms(5) True
       using order_le_less_trans
       by blast
   qed
 next
   case False
   show ?thesis
     apply (rule exI [of _ "{}"])
     using False assms(2,4,5,7)
     by simp
 qed
 
 section \<open>Properties of the upper edge bound\<close>
 
 text \<open>In this section we prove results about the upper edge bound in Tur\'{a}n's theorem.
 The first lemma proves that upper bounds of the sizes of the partitions sum up exactly to the overall upper bound.\<close>
 
 lemma turan_sum_eq :
   fixes n p :: nat
   assumes "p \<ge> 2" and "p \<le> n"
   shows "(p-1) * (p-2) / 2 + (1 - 1 / (p-1)) * (n - p + 1) ^ 2 / 2 + (p - 2) * (n - p + 1) = (1 - 1 / (p-1)) * n^2 / 2"
 proof -
   have "a * (a-1) / 2 + (1 - 1 / a) * (n - a) ^ 2 / 2 + (a - 1) * (n - a)  = (1 - 1 / a) * n^2 / 2"
     if a1: "a \<ge> 1" and a2: "n \<ge> a"
     for a :: nat
   proof -
     have "a\<^sup>2 + (n - a)\<^sup>2 + a * (n - a) * 2 = n\<^sup>2"
       using a2
       apply (simp flip: Groups.ab_semigroup_mult_class.mult.commute [of 2 "a * (n - a)"])
       apply (simp add: Semiring_Normalization.comm_semiring_1_class.semiring_normalization_rules(18) [of 2 a "(n - a)"])
       by (simp flip: Power.comm_semiring_1_class.power2_sum [of a "n-a"])
     then have "((a - 1) / a) * (a ^ 2 + (n - a) ^ 2 + a * (n - a) * 2) = ((a - 1) / a) * n^2"
       by presburger
     then have "(((a - 1) / a) * a ^ 2 + ((a - 1) / a) * (n - a) ^ 2 + ((a - 1) / a) * a * (n - a) * 2) = ..."
       using Rings.semiring_class.distrib_left [of "(a - 1) / a" "a\<^sup>2 + (n - a)\<^sup>2" "a * (n - a) * 2"]
       using Rings.semiring_class.distrib_left [of "(a - 1) / a" "a\<^sup>2" "(n - a)\<^sup>2"]
       by auto
     moreover have "((a - 1) / a) * a ^ 2 = a * (a-1)"
       by (simp add: power2_eq_square)
     ultimately have "a * (a-1) + ((a - 1) / a) * (n - a) ^ 2 + (a - 1) * (n - a) * 2  = ((a - 1) / a) * n^2"
       using a1 a2
       by auto
     moreover have "1 - 1 / a = (a - 1) / a"
       by (smt (verit, del_insts) One_nat_def Suc_pred diff_divide_distrib diff_is_0_eq of_nat_1 of_nat_diff of_nat_le_0_iff of_nat_le_iff of_nat_less_iff right_inverse_eq that)
     ultimately have "a * (a-1) + (1 - 1 / a) * (n - a) ^ 2 + (a - 1) * (n - a) * 2  = (1 - 1 / a) * n^2"
       by simp
     then show ?thesis
       by simp
   qed
   moreover have "p - 1 \<ge> 1"
     using \<open>p \<ge> 2\<close> by auto
   moreover have "n \<ge> p - 1"
     using assms(2) by auto
   ultimately show ?thesis
     by (smt (verit) assms Nat.add_diff_assoc2 Nat.diff_diff_right diff_diff_left le_eq_less_or_eq less_Suc_eq_le linorder_not_less nat_1_add_1 plus_1_eq_Suc)
 qed
 
 text \<open>The next fact proves that the upper bound of edges is monotonically increasing with the size of the biggest clique.\<close>
 
 lemma turan_mono :
   fixes n p q :: nat
   assumes "0 < q" and "q < p" and "p \<le> n"
   shows "(1 - 1 / q) * n^2 / 2 \<le> (1 - 1 / (p-1)) * n^2 / 2"
   using assms
   by (simp add: Extended_Nonnegative_Real.divide_right_mono_ennreal Real.inverse_of_nat_le)
 
 section \<open>Tur\'{a}n's Graph Theorem\<close>
 
 text \<open>In this section we turn to the direct adaptation of Tur\'{a}n's original proof as presented by Aigner and Ziegler \cite{Aigner2018}\<close>
 
 theorem turan :
   fixes p n :: nat
   assumes "finite (uverts G)"
     and "uwellformed G" and "\<forall>C p'. uclique C G p' \<longrightarrow> p' < p" and "p \<ge> 2" and "card(uverts G) = n"
   shows "card (uedges G) \<le> (1 - 1 / (p-1)) * n^2 / 2" using assms
 proof (induction n arbitrary: G rule: less_induct)
   case (less n)
   then show ?case
   proof (cases "n < p")
     case True
     show ?thesis
     proof (cases "n")
       case 0
       with less True show ?thesis
         by (auto simp add: wellformed_uverts_0)
     next
       case (Suc n')
       with True have "(1 - 1 / real n) \<le> (1 - 1 / real (p - 1))"
         by (metis diff_Suc_1 diff_left_mono inverse_of_nat_le less_Suc_eq_le linorder_not_less list_decode.cases not_add_less1 plus_1_eq_Suc)
       moreover have "real (card (uedges G)) \<le> (1 - 1 / real n) * real (n\<^sup>2) / 2"
         using ugraph_max_edges [OF less(3,6,2)]
         by (smt (verit, ccfv_SIG) left_diff_distrib mult.right_neutral mult_of_nat_commute nonzero_mult_div_cancel_left of_nat_1 of_nat_mult power2_eq_square times_divide_eq_left)
       ultimately show ?thesis
         using Rings.ordered_semiring_class.mult_right_mono divide_less_eq_numeral1(1) le_less_trans linorder_not_less of_nat_0_le_iff
         by (smt (verit, ccfv_threshold) divide_nonneg_nonneg times_divide_eq_right)
     qed
   next
     case False
     show ?thesis
     proof -
       obtain C q where C: "uclique C G q"
         and C_max: "(\<forall>C q'. uclique C G q' \<longrightarrow> q' \<le> q)"
         and q: "q < card (uverts G)"
         using clique_exists_gt0 [OF \<open>finite (uverts G)\<close>] False \<open>p \<ge> 2\<close> less.prems(1,3,5)
         by (metis card.empty card_gt_0_iff le_eq_less_or_eq order_less_le_trans pos2)
       obtain E C' where E: "uwellformed (uverts G, uedges G \<union> E)"
         and C': "(uclique C' (uverts G, uedges G \<union> E) (p-1))"
         and C'_max: "(\<forall>C q'. uclique C (uverts G, uedges G \<union> E) q' \<longrightarrow> q' \<le> p-1)"
         using clique_add_edges_max [OF \<open>finite (uverts G)\<close> \<open>uwellformed G\<close> q _ C_max, of "p-1"]
         using C less(4) less(5) False \<open>card (uverts G) = n\<close>
         by (smt (verit) One_nat_def Suc_leD Suc_pred less_Suc_eq_le linorder_not_less order_less_le_trans pos2)
       have "card {e \<in> uedges G \<union> E. e \<subseteq> uverts C'} = (p-1) * (p-2) / 2"
         using clique_edges_inside [OF E _ _ _ C'] False less(2) less.prems(4) C'
         by (smt (verit, del_insts) Collect_cong Suc_1 add_leD1 clique_max_size fst_conv of_nat_1 of_nat_add of_nat_diff of_nat_mult plus_1_eq_Suc snd_conv)
       moreover have "card {e \<in> uedges G \<union> E. e \<subseteq> uverts G - uverts C'} \<le> (1 - 1 / (p-1)) * (n - p + 1) ^ 2 / 2"
       proof -
         have "real(card{e \<in> uedges (uverts G, uedges G \<union> E). e \<subseteq> uverts (uverts G, uedges G \<union> E) - uverts C'})
               \<le> (1 - 1 / (real p - 1)) * (real n - real p + 1)\<^sup>2 / 2"
           using clique_edges_outside [OF E _ less(5) _ _ C' C'_max, of n] linorder_class.leI [OF False] less(1,2,6)
           by (metis (no_types, lifting) fst_conv)
         then show ?thesis
           by (simp, smt (verit, best) False One_nat_def Suc_1 Suc_leD add.commute leI less.prems(4) of_nat_1 of_nat_diff)
       qed
       moreover have "card {e \<in> uedges G \<union> E. e \<inter> uverts C' \<noteq> {} \<and> e \<inter> (uverts G - uverts C') \<noteq> {}} \<le> (p - 2) * (n - p + 1)"
         using clique_edges_inside_to_outside [OF E _ _ _ _ C' C'_max, of  n] less(2,5,6)
         by (simp, metis (no_types, lifting) C' False Nat.add_diff_assoc Nat.add_diff_assoc2 One_nat_def Suc_1 clique_max_size fst_conv leI mult_Suc_right plus_1_eq_Suc)
       ultimately have "real (card (uedges G \<union> E)) \<le> (1 - 1 / real (p - 1)) * real (n\<^sup>2) / 2"
         using graph_partition_edges_card [OF _ E, of "uverts C'"]
         using less(2) turan_sum_eq [OF \<open>2 \<le> p\<close>, of n] False C' uclique_def subgraph_def
         by (smt (verit) Collect_cong fst_eqD linorder_not_le of_nat_add of_nat_mono snd_eqD)
       then show ?thesis
         using less(2) E finite_verts_edges Finite_Set.card_mono [OF _ Set.Un_upper1 [of "uedges G" E]]
         by force
     qed
   qed
 qed
 
 section \<open>A simplified proof of Tur\'{a}n's Graph Theorem\<close>
 
 text \<open>In this section we discuss a simplified proof of Tur\'{a}n's Graph Theorem which uses an idea put forward by the author:
 Instead of increasing the size of the biggest clique it is also possible to use the fact that
 the expression in Tur\'{a}n's graph theorem is monotonically increasing in the size of the biggest clique (Lemma @{thm [source] turan_mono}).
 Hence, it suffices to prove the upper bound for the actual biggest clique size in the graph.
 Afterwards, the monotonicity provides the desired inequality.
 
 The simplifications in the proof are annotated accordingly.\<close>
 
 theorem turan' :
   fixes p n :: nat
   assumes "finite (uverts G)"
     and "uwellformed G" and "\<forall>C p'. uclique C G p' \<longrightarrow> p' < p" and "p \<ge> 2" and "card(uverts G) = n"
   shows "card (uedges G) \<le> (1 - 1 / (p-1)) * n^2 / 2" using assms
 proof (induction n arbitrary: p G rule: less_induct)
   txt \<open>In the simplified proof we also need to generalize over the biggest clique size @{term p}
        so that we can leverage the induction hypothesis in the proof
        for the already pre-existing biggest clique size which might be smaller than @{term "p-1"}.\<close>
   case (less n)
   then show ?case
   proof (cases "n < p")
     case True
     show ?thesis
     proof (cases "n")
       case 0
       with less True show ?thesis
         by (auto simp add: wellformed_uverts_0)
     next
       case (Suc n')
       with True have "(1 - 1 / real n) \<le> (1 - 1 / real (p - 1))"
         by (metis diff_Suc_1 diff_left_mono inverse_of_nat_le less_Suc_eq_le linorder_not_less list_decode.cases not_add_less1 plus_1_eq_Suc)
       moreover have "real (card (uedges G)) \<le> (1 - 1 / real n) * real (n\<^sup>2) / 2"
         using ugraph_max_edges [OF less(3,6,2)]
         by (smt (verit, ccfv_SIG) left_diff_distrib mult.right_neutral mult_of_nat_commute nonzero_mult_div_cancel_left of_nat_1 of_nat_mult power2_eq_square times_divide_eq_left)
       ultimately show ?thesis
         using Rings.ordered_semiring_class.mult_right_mono divide_less_eq_numeral1(1) le_less_trans linorder_not_less of_nat_0_le_iff
         by (smt (verit, ccfv_threshold) divide_nonneg_nonneg times_divide_eq_right)
     qed
   next
     case False
     show ?thesis
     proof -
       from False \<open>p \<ge> 2\<close>
       obtain C q where C: "uclique C G q"
         and C_max: "(\<forall>C q'. uclique C G q' \<longrightarrow> q' \<le> q)"
         and q1: "q < card (uverts G)" and q2: "0 < q"
         and pq: "q < p"
         using clique_exists_gt0 [OF \<open>finite (uverts G)\<close>] clique_exists1 less.prems(1,3,5)
         by (metis card.empty card_gt_0_iff le_eq_less_or_eq order_less_le_trans pos2)
       txt \<open>In the unsimplified proof we extend this existing greatest clique C to a clique of size @{term "p-1"}.
            This part is made superfluous in the simplified proof.
            In particular, also Section \ref{sec:extend_clique} is unneeded for this simplified proof.
            From here on the proof is analogous to the unsimplified proof
            with the potentially smaller clique of size @{term q} in place of the extended clique.\<close>
       have "card {e \<in> uedges G. e \<subseteq> uverts C} = q * (q-1) / 2"
         using clique_edges_inside [OF less(3,2) _ _ C] q1 less(6)
         by auto
       moreover have "card {e \<in> uedges G. e \<subseteq> uverts G - uverts C} \<le> (1 - 1 / q) * (n - q) ^ 2 / 2"
       proof -
         have "real (card {e \<in> uedges G. e \<subseteq> uverts G - uverts C})
               \<le> (1 - 1 / (real (q + 1) - 1)) * (real n - real (q + 1) + 1)\<^sup>2 / 2"
           using clique_edges_outside [OF less(3,2) _ _ , of "q+1" n C] C C_max q1 q2 linorder_class.leI [OF False] less(1,6)
           by (smt (verit, ccfv_threshold) Suc_1 Suc_eq_plus1 Suc_leI diff_add_inverse2 zero_less_diff)
         then show ?thesis
           using  less.prems(5) q1
           by (simp add: of_nat_diff)
       qed
       moreover have "card {e \<in> uedges G. e \<inter> uverts C \<noteq> {} \<and> e \<inter> (uverts G - uverts C) \<noteq> {}} \<le> (q - 1) * (n - q)"
         using clique_edges_inside_to_outside [OF less(3,2) q2 _ less(6) C C_max] q1
         by simp
       ultimately have "real (card (uedges G)) \<le> (1 - 1 / real q) * real (n\<^sup>2) / 2"
         using graph_partition_edges_card [OF less(2,3), of "uverts C"]
         using C uclique_def subgraph_def q1 q2 less.prems(5) turan_sum_eq [of "Suc q" n]
         by (smt (verit) Nat.add_diff_assoc Suc_1 Suc_le_eq Suc_le_mono add.commute add.right_neutral diff_Suc_1 diff_Suc_Suc of_nat_add of_nat_mono plus_1_eq_Suc)
       then show ?thesis
         txt \<open>The final statement can then easily be derived with the monotonicity (Lemma @{thm [source] turan_mono}).\<close>
         using turan_mono [OF q2 pq, of n] False
         by linarith
     qed
   qed
 qed
 
 end