Theory First_Welfare_Theorem.Preferences

(* License: LGPL *)
(*
Author: Julian Parsert <julian.parsert@gmail.com>
Author: Cezary Kaliszyk
*)

section ‹Preference Relations›

text ‹ Preferences modeled as a set of pairs ›

theory Preferences
  imports
    "HOL-Analysis.Multivariate_Analysis"
    Syntax
begin


subsection ‹Basic Preference Relation›

text ‹ Basic preference relation locale with carrier and relation modeled as a set of pairs. ›

locale preference =
  fixes carrier :: "'a set"
  fixes relation :: "'a relation"
  assumes not_outside: "(x,y)  relation  x  carrier"
    and "(x,y)  relation  y  carrier"
  assumes trans_refl: "preorder_on  carrier relation"

context preference
begin

no_notation eqpoll (infixl "" 50)

abbreviation geq ("_  _" [51,51] 60)
  where
    "x  y  x ≽[relation] y"

abbreviation str_gr ("_  _" [51,51] 60)
  where
    "x  y  x  y  ¬y  x"

abbreviation indiff ("_  _" [51,51] 60)
  where
    "x  y  x  y  y  x"

lemma reflexivity: "refl_on carrier relation"
  using preorder_on_def trans_refl by blast

lemma transitivity: "trans relation"
  using preorder_on_def trans_refl by auto

lemma indiff_trans [simp]: "x  y  y  z  x  z"
  by (meson transE transitivity)

end


subsubsection ‹ Contour sets ›

definition at_least_as_good :: "'a  'a set  'a relation  'a set"
  where
    "at_least_as_good x B P = {y  B. y ≽[P] x }"

definition no_better_than :: "'a  'a set  'a relation  'a set"
  where
    "no_better_than x B P = {y  B. x ≽[P] y}"

definition as_good_as :: "'a  'a set  'a relation  'a set"
  where
    "as_good_as x B P = {y  B. x ≈[P] y}"

lemma at_lst_asgd_ge:
  assumes "x  at_least_as_good y B Pr"
  shows "x ≽[Pr] y"
  using assms at_least_as_good_def by fastforce

lemma strict_contour_is_diff:
  "{a  B. a ≻[Pr] y} = at_least_as_good y B Pr - as_good_as y B Pr"
  by(auto simp add: at_least_as_good_def as_good_as_def)

lemma strict_countour_def [simp]:
  "(at_least_as_good y B Pr) - as_good_as y B Pr = {x  B. x ≻[Pr] y}"
  by (simp add: as_good_as_def at_least_as_good_def strict_contour_is_diff)

lemma at_least_as_goodD [dest]:
  assumes "z  at_least_as_good y B Pr"
  shows "z ≽[Pr] y"
  using assms at_least_as_good_def by fastforce


subsection ‹Rational Preference Relation›

text ‹ Rational preferences add totality to the basic preferences. ›

locale rational_preference = preference +
  assumes total: "total_on carrier relation"
begin

lemma compl: "x  carrier . y carrier . x  y  y  x"
  by (metis refl_onD reflexivity total total_on_def)

lemma strict_not_refl_weak [iff]: "x  carrier  y  carrier  ¬ (y  x)  x  y"
  by (metis refl_onD reflexivity total total_on_def)

lemma strict_trans [simp]: "x  y  y  z  x  z"
  by (meson transE transitivity)

lemma completeD [dest]: "x  carrier  y  carrier  x  y  x  y  y  x"
  by blast

lemma pref_in_at_least_as:
  assumes "x  y"
  shows "x  at_least_as_good y carrier relation"
  by (metis (no_types, lifting) CollectI assms
      at_least_as_good_def preference.not_outside preference_axioms)

lemma worse_in_no_better:
  assumes "x  y"
  shows "y  no_better_than y carrier relation"
  by (metis (no_types, lifting) CollectI assms no_better_than_def
      preference_axioms preference_def strict_not_refl_weak)

lemma strict_is_neg_transitive :
  assumes "x  carrier  y  carrier  z  carrier"
  shows "x  y  x  z  z  y"
  by (meson assms compl transE transitivity)

lemma weak_is_transitive:
 assumes "x  carrier  y  carrier  z  carrier"
 shows "x  y  y  z  x  z"
  by (meson transD transitivity)

lemma no_better_than_nonepty:
  assumes "carrier  {}"
  shows "x. x  carrier  (no_better_than x carrier relation)  {}"
  by (metis (no_types, lifting) empty_iff mem_Collect_eq
      no_better_than_def refl_onD reflexivity)

lemma no_better_subset_pref :
  assumes "x  y"
  shows "no_better_than y carrier relation  no_better_than x carrier relation"
proof
  fix a
  assume "a  no_better_than y carrier relation"
  then show "a  no_better_than x carrier relation"
    by (metis (no_types, lifting) assms mem_Collect_eq no_better_than_def transE transitivity)
qed

lemma no_better_thansubset_rel :
  assumes "x  carrier" and "y  carrier"
  assumes "no_better_than y carrier relation  no_better_than x carrier relation"
  shows "x  y"
proof -
  have  "{a  carrier. y  a}  {a  carrier. x  a}"
    by (metis (no_types) assms(3) no_better_than_def)
  then show ?thesis
    by (metis (mono_tags, lifting) Collect_mono_iff assms(2) compl)
qed

lemma nbt_nest :
  shows "(no_better_than y carrier relation  no_better_than x carrier relation) 
        (no_better_than x carrier relation  no_better_than y carrier relation)"
  by (metis (no_types, lifting) CollectD compl no_better_subset_pref no_better_than_def not_outside subsetI)

lemma at_lst_asgd_not_ge:
  assumes "carrier  {}"
  assumes "x  carrier" and "y  carrier"
  assumes "x  at_least_as_good y carrier relation"
  shows "¬ x  y"
  by (metis (no_types, lifting) CollectI assms(2) assms(4) at_least_as_good_def)

lemma as_good_as_sameIff[iff]:
  "z  as_good_as y carrier relation  z  y  y  z"
  by (metis (no_types, lifting) as_good_as_def mem_Collect_eq not_outside)

lemma same_at_least_as_equal:
  assumes "z  y"
  shows "at_least_as_good z carrier relation =
         at_least_as_good y carrier relation" (is "?az = ?ay")
proof
  have "z  carrier  y  carrier"
    by (meson assms refl_onD2 reflexivity)
  moreover have "x  carrier. x  z  x  y"
    by (meson assms transD transitivity)
  ultimately show "?az  ?ay"
    by (metis at_lst_asgd_ge at_lst_asgd_not_ge
        equals0D not_outside subsetI)
next
   have "z  carrier  y  carrier"
    by (meson assms refl_onD2 reflexivity)
  moreover have "x  carrier. x  y  x  z"
    by (meson assms transD transitivity)
  ultimately show "?ay  ?az"
    by (metis at_lst_asgd_ge at_lst_asgd_not_ge
        equals0D not_outside subsetI)
qed

lemma as_good_asIff [iff]:
  "x  as_good_as y carrier relation  x ≈[relation] y"
  by blast

lemma nbt_subset:
  assumes "finite carrier"
  assumes "x  carrier" and "y  carrier"
  shows "no_better_than x carrier relation  no_better_than x carrier relation 
         no_better_than x carrier relation  no_better_than x carrier relation"
  by auto

lemma fnt_carrier_fnt_rel: "finite carrier  finite relation"
  by (metis finite_SigmaI refl_on_def reflexivity rev_finite_subset)

lemma nbt_subset_carrier:
  assumes "x  carrier"
  shows "no_better_than x carrier relation  carrier"
  using no_better_than_def by fastforce

lemma xy_in_eachothers_nbt:
  assumes "x  carrier" "y  carrier"
  shows "x  no_better_than y carrier relation 
         y  no_better_than x carrier relation"
  by (meson assms(1) assms(2) contra_subsetD nbt_nest refl_onD reflexivity worse_in_no_better)

lemma same_nbt_same_pref:
  assumes "x  carrier" "y  carrier"
  shows "x  no_better_than y carrier relation 
         y  no_better_than x carrier relation  x  y"
    by (metis (mono_tags, lifting) CollectD contra_subsetD no_better_subset_pref
        no_better_than_def worse_in_no_better)

lemma indifferent_imp_weak_pref: 
  assumes "x  y"
  shows" x  y" "y  x"
  by (simp add: assms)+

subsection ‹ Finite carrier›

context
  assumes "finite carrier"
begin

lemma fnt_carrier_fnt_nbt:
  shows "xcarrier. finite (no_better_than x carrier relation)"
proof
  fix x
  assume "x  carrier"
  then show "finite (no_better_than x carrier relation)"
  using  finite_subset nbt_subset_carrier finite carrier by blast
qed

lemma nbt_subset_imp_card_leq:
  assumes "x  carrier" and "y  carrier"
  shows "no_better_than x carrier relation  no_better_than y carrier relation 
  card (no_better_than x carrier relation)  card  (no_better_than y carrier relation)"
  (is "?nbt  ?card")
proof
  assume "?nbt"
  then show "?card"
    by (simp add: assms(2) card_mono fnt_carrier_fnt_nbt)
next
  assume "?card"
  then show "?nbt"
    by (metis  assms(1) card_seteq fnt_carrier_fnt_nbt nbt_nest)
qed

lemma card_leq_pref:
  assumes "x  carrier" and "y  carrier"
  shows "card (no_better_than x carrier relation)  card (no_better_than y carrier relation)
    y  x"
proof (rule iffI, goal_cases)
  case 1
  then show ?case
    using assms(1) assms(2) nbt_subset_imp_card_leq no_better_thansubset_rel by presburger
next
  case 2
  then show ?case
    using assms(1) assms(2) nbt_subset_imp_card_leq no_better_subset_pref by blast
qed

lemma finite_ne_remove_induct:
  assumes "finite B" "B  {}"
    "A. finite A   A  B  A  {} 
         (x. x  A  A - {x}  {}  P (A - {x}))  P A"
  shows "P B"
  by (metis assms finite_remove_induct[where P = "λF. F = {}  P F" for P])


lemma finite_nempty_preorder_has_max:
  assumes "finite B" "B  {}" "refl_on B R" "trans R" "total_on B R"
  shows "x  B. y  B. (x, y)  R"
  using assms(1) subset_refl[of B] assms(2)
proof (induct B rule: finite_subset_induct)
  case (insert x F)
  then show ?case using assms(3-)
    by (cases "F = {}") (auto simp: refl_onD total_on_def, metis refl_onD2 transE)
qed auto

lemma finite_nempty_preorder_has_min:
  assumes "finite B" "B  {}" "refl_on B R" "trans R" "total_on B R"
  shows "x  B. y  B. (y, x)  R"
  using assms(1) subset_refl[of B] assms(2)
proof (induct B rule: finite_subset_induct)
  case (insert x F)
  then show ?case using assms(3-)
    by (cases "F = {}") (auto simp: refl_onD total_on_def, metis refl_onD2 transE)
qed auto

lemma finite_nonempty_carrier_has_maximum:
  assumes "carrier  {}"
  shows "e  carrier. m  carrier. e ≽[relation] m"
  using finite_nempty_preorder_has_max[of carrier relation] assms
     finite carrier reflexivity total transitivity by blast

lemma finite_nonempty_carrier_has_minimum:
  assumes "carrier  {}"
  shows "e  carrier. m  carrier. m ≽[relation] e"
  using finite_nempty_preorder_has_min[of carrier relation] assms
     finite carrier reflexivity total transitivity by blast

end (*finite carrier*)


lemma all_carrier_ex_sub_rel: 
  "c  carrier. r  relation. rational_preference c r"
proof (standard,standard)
  fix c
  assume c_in: "c  carrier"
  define r' where
    "r' = {(x,y)  relation. x  c  y  c}"
  have r'_sub: "r'  c × c"
    using r'_def by blast
  have "x  c. x ≽[r'] x"
    by (metis (no_types, lifting) CollectI c_in case_prodI compl r'_def subsetCE)
  then have refl: "refl_on c r'"
    by (meson r'_sub refl_onI)
  have trans: "trans r'"
  proof
    fix x y z
    assume a1: "x ≽[r'] y"
    assume a2: "y ≽[r'] z"
    show " x ≽[r'] z"
      by (metis (mono_tags, lifting) CollectD CollectI a1 a2 case_prodD case_prodI r'_def transE transitivity)
  qed
  have total: "total_on c r'"
  proof (standard)
    fix x y
    assume a1:"x  c"
    assume a2: "y  c"
    assume a3: "x  y"
    show "x ≽[r'] y  y ≽[r'] x "
      by (metis (no_types, lifting) CollectI a1 a2 c_in case_prodI compl r'_def subset_iff)
  qed
  have "rational_preference c r'"
    by (meson local.refl local.trans preference.intro preorder_on_def rational_preference.intro 
        rational_preference_axioms.intro refl_on_domain total)
  thus "rrelation. rational_preference c r"
    by (metis (no_types, lifting) CollectD case_prodD r'_def subrelI)
qed

end (*rational preference*)


subsection ‹ Local Non-Satiation ›

text ‹ Defining local non-satiation. ›

definition local_nonsatiation
  where
  "local_nonsatiation B P 
   (xB. e>0. yB. norm (y - x)  e  y ≻[P] x)"

text ‹ Alternate definitions and intro/dest rules with them ›

lemma lns_alt_def1 [iff] :
  shows "local_nonsatiation B P  (x  B. e>0. (y  B. dist y x  e  y ≻[P] x))"
  by(simp add : dist_norm local_nonsatiation_def)

lemma lns_normI [intro]:
  assumes "x e. x  B  e > 0  (yB. norm (y - x)  e  y ≻[P] x)"
  shows "local_nonsatiation B P"
  by (simp add: assms dist_norm)

lemma lns_distI [intro]:
  assumes "x e. x  B  e > 0  (yB. (dist y x)  e  y ≻[P] x)"
  shows "local_nonsatiation B P"
  by (meson lns_alt_def1 assms)

lemma lns_alt_def2 [iff]:
  "local_nonsatiation B P  (xB. e>0. (y.  y  (ball x e)  y  B  y ≻[P] x))"
proof
  assume "local_nonsatiation B P"
  then show "xB. e>0. x'. x'  ball x e  x'  B  x' ≻[P] x"
    by (auto simp add : ball_def) (metis dense le_less_trans dist_commute)
next
  assume "xB. e>0. y. y  ball x e  y  B  y ≻[P] x"
  then show "local_nonsatiation B P"
    by (metis (no_types, lifting) ball_def dist_commute
        less_le_not_le lns_alt_def1 mem_Collect_eq)
qed

lemma lns_normD [dest]:
  assumes "local_nonsatiation B P"
  shows "x  B. e>0. y  B. (norm (y - x)  e  y ≻[P] x)"
  by (meson assms local_nonsatiation_def)


subsection ‹ Convex preferences ›

definition weak_convex_pref :: "('a::real_vector) relation  bool"
  where
    "weak_convex_pref Pr  (x y. x ≽[Pr] y 
      (α β. α + β = 1  α > 0  β > 0  α *R x + β *R y ≽[Pr] y))"

definition convex_pref :: "('a::real_vector) relation  bool"
  where
    "convex_pref Pr  (x y. x ≻[Pr] y 
      (α. 1 > α  α > 0  α *R x + (1-α) *R y ≻[Pr] y))"

definition strict_convex_pref :: "('a::real_vector) relation  bool"
  where
    "strict_convex_pref Pr  (x y. x ≽[Pr] y  x  y 
      (α. 1 > α  α > 0  α *R x + (1-α) *R y ≻[Pr] y))"

lemma convex_ge_imp_conved:
  assumes "x y. x ≽[Pr] y  (α β. α + β = 1  α  0  β  0  α *R x + β *R y ≽[Pr] y)"
  shows "weak_convex_pref Pr"
  by (simp add: assms weak_convex_pref_def)

lemma weak_convexI [intro]:
  assumes "x y α β. x ≽[Pr] y  α + β = 1  0 < α  0 < β  α *R x + β *R y ≽[Pr] y"
  shows "weak_convex_pref Pr"
  by (simp add: assms weak_convex_pref_def)

lemma weak_convexD [dest]:
  assumes "weak_convex_pref Pr" and "x ≽[Pr] y" and "0 < u" and "0 < v" and "u + v = 1"
  shows "u *R x + v *R y ≽[Pr] y"
    using assms weak_convex_pref_def by blast


subsection ‹ Real Vector Preferences ›

text ‹ Preference relations on real vector type class. ›

locale real_vector_rpr = rational_preference carrier relation
for carrier :: "'a::real_vector set"
and relation :: "'a relation"

sublocale  real_vector_rpr  rational_preference carrier relation
  by (simp add: rational_preference_axioms)

context real_vector_rpr
begin

lemma have_rpr: "rational_preference carrier relation"
  by (simp add: rational_preference_axioms)

text ‹ Multiple convexity alternate definitions intro/dest rules. ›

lemma weak_convex1D [dest]:
  assumes "weak_convex_pref relation" and "x ≽[relation] y" and "0  u" and "0  v" and "u + v = 1"
  shows "u *R x + v *R y ≽[relation] y"
proof-
  have u_0: "u = 0  u *R x + v *R y ≽[relation] y"
  proof
    assume u_0: "u = 0"
    have "v = 1"
      using assms(5) u_0 by auto
    then have "?thesis"
      by (metis add.left_neutral assms(2) preference.reflexivity preference_axioms
          real_vector.scale_zero_left refl_onD2 scaleR_one strict_not_refl_weak)
    thus "u *R x + v *R y ≽[relation] y "
      using u_0 by blast
  qed
  have "u  0  u  1  u *R x + v *R y ≽[relation] y"
    by (metis add_cancel_right_right antisym_conv not_le assms weak_convexD )
  then show ?thesis
    by (metis u_0 assms(2,5) add_cancel_right_right real_vector.scale_zero_left scaleR_one)
qed

lemma weak_convex1I [intro] :
  assumes "x. convex (at_least_as_good x carrier relation)"
  shows "weak_convex_pref relation"
proof (rule weak_convexI)
  fix x and y and α β :: real
  assume assum : "x ≽[relation] y"
  assume reals: "0 < α" "0 < β" " α + β = 1"
  then have "x  carrier"
    by (meson assum preference.not_outside rational_preference.axioms(1) have_rpr)
  have "y  carrier"
    by (meson assum refl_onD2 reflexivity)
  then have y_in_upper_cont: "y  (at_least_as_good y carrier relation)"
    using assms rational_preference.at_lst_asgd_not_ge
      rational_preference.compl  by (metis empty_iff have_rpr)
  then have "x  (at_least_as_good y carrier relation)"
    using assum pref_in_at_least_as by blast
  moreover have "0  β" and "0  α"
    using reals by (auto)
  ultimately show "(α *R x + β *R y) ≽[relation] y"
    by (meson assms(1) at_least_as_goodD convexD reals(3) y_in_upper_cont)
qed

text ‹ Definition of convexity in "Handbook of Social Choice and Welfare"cite"arrow2010handbook". ›

lemma convex_def_alt:
  assumes "rational_preference carrier relation"
  assumes "weak_convex_pref relation"
  shows "(x  carrier. convex (at_least_as_good x carrier relation))"
proof
  fix x
  assume x_in: "x  carrier"
  show "convex (at_least_as_good x carrier relation)" (is "convex ?x")
  proof (rule convexI)
    fix a b :: "'a" and  α :: "real" and β :: "real"
    assume a_in: "a  ?x"
    assume b_in: "b  ?x"
    assume reals: " 0  α" "0  β" "α + β = 1"
    have a_g_x: "a ≽[relation] x"
      using a_in by blast
    have b_g_x: "b ≽[relation] x"
      using b_in by blast
    have "a ≽[relation] b  b ≽[relation] a"
      by (meson a_in at_least_as_goodD b_in preference.not_outside
          rational_preference.compl rational_preference_def assms(1))
    then show "α *R a + β *R b  ?x"
    proof(rule disjE)
      assume "a ≽[relation] b"
      then have "α *R a + β *R b  ≽[relation] b"
        using assms reals by blast
      then have "α *R a + β *R b ≽[relation] x"
        by (meson b_g_x  assms(1) preference.not_outside x_in
            rational_preference.strict_is_neg_transitive
            rational_preference.strict_not_refl_weak rational_preference_def)
      then show ?thesis
        by (metis (no_types, lifting) CollectI  assms(1)
            at_least_as_good_def preference_def rational_preference_def)
    next
      assume as: "b ≽[relation] a"
      then have "α *R a + β *R b ≽[relation] a"
        by (metis add.commute assms(2) reals weak_convex1D)
      have "α *R a + β *R b ≽[relation] a"
        by (metis as add.commute  assms(2)
            reals(1,2,3) weak_convex1D)
      then have "α *R a + β *R b ≽[relation] x"
        by (meson a_g_x assms(1) preference.indiff_trans x_in
            preference.not_outside rational_preference.axioms(1)
            rational_preference.strict_is_neg_transitive )
      then show ?thesis
        using pref_in_at_least_as by blast
    qed
  qed
qed

lemma convex_imp_convex_str_upper_cnt:
  assumes "x  carrier. convex (at_least_as_good x carrier relation)"
  shows "convex (at_least_as_good x carrier relation - as_good_as x carrier relation)"
    (is "convex ( ?a - ?b)")
proof (rule convexI)
  fix a y u v
  assume as_a: "a  ?a - ?b"
  assume as_y: "y  ?a - ?b"
  assume reals: "0  (u::real)" "0  v" "u + v = 1"
  have cvx: "weak_convex_pref relation "
    by (meson assms at_least_as_goodD convexI have_rpr
        preference_def rational_preference.axioms(1) weak_convex1I)
  then have a_g_x: "a ≻[relation] x"
    using as_a by blast
  then have y_gt_x: "y ≻[relation] x"
    using as_y by blast
  show "u *R a + v *R y  ?a - ?b"
  proof
    show "u *R a + v *R y  ?a"
      by (metis DiffD1 a_g_x as_a as_y assms convexD reals have_rpr
          preference_def rational_preference.axioms(1))
  next
    have "a ≽[relation] y  y ≽[relation] a"
      by (meson a_g_x y_gt_x assms(1) preference.not_outside have_rpr
          rational_preference.axioms(1) rational_preference.strict_not_refl_weak)
    then show "u *R a + v *R y  ?b"
    proof
      assume "a ≽[relation] y"
      then have "u *R a + v *R y ≽[relation] y"
        using cvx assms(1) reals by blast
      then have "u *R a + v *R y ≻[relation] x"
        using y_gt_x by (meson assms(1) rational_preference.axioms(1) have_rpr
            rational_preference.strict_is_neg_transitive preference_def)
      then show "u *R a + v *R y  as_good_as x carrier relation"
        by blast
    next
      assume "y ≽[relation] a"
      then have "u *R a + v *R y ≽[relation] a"
        using cvx assms(1) reals by (metis add.commute weak_convex1D)
      then have "u *R a + v *R y ≻[relation] x"
        by (meson a_g_x assms(1) rational_preference.strict_is_neg_transitive
            rational_preference.axioms(1) preference_def have_rpr)
      then show "u *R a + v *R y  ?b"
        by blast
    qed
  qed
qed

end

subsubsection ‹ Monotone preferences ›

definition weak_monotone_prefs :: "'a set  ('a::ord) relation  bool"
  where
    "weak_monotone_prefs B P  (x  B. y  B. x  y  x ≽[P]y)"

definition monotone_preference :: "'a set  ('a::ord) relation  bool"
  where
    "monotone_preference B P  (x  B. y  B. x > y  x ≻[P] y)"


text ‹ Given a carrier set that is unbounded above (not the "standard" mathematical definition),
       monotonicity implies local non-satiation. ›

lemma unbounded_above_mono_imp_lns:
  assumes "M  carrier. (x > M. x  carrier)"
  assumes mono: "monotone_preference (carrier:: 'a::ordered_euclidean_space set) relation"
  shows "local_nonsatiation carrier relation"
proof(rule lns_distI)
  fix x and e::"real"
  assume x_in: "x  carrier"
  assume gz : "e > 0"
  show "ycarrier. dist y x  e  y ≽[relation] x  (x, y)  relation"
  proof-
    obtain v :: real where
      v:"v < e" "0 < v" using gz dense by blast
    obtain i where
      i:"(i::'a)  Basis" by fastforce
    define y where
      y_value : "y = x + v *R i"
    have ge:"y  x"
      using y_value i unfolding y_value
      by (simp add: v(2) zero_le_scaleR_iff)
    have "y  x"
      using y_value i unfolding y_value
      using v(2) by auto
    hence y_str_g_x : "y > x"
      using ge by auto
    have y_in: "y  carrier"
      using assms(1) x_in y_str_g_x by blast
    then have y_pref_x : "y ≻[relation] x"
      using y_str_g_x x_in mono monotone_preference_def  by blast
    hence " norm (y - x)  e"
      using 0 < v y_value y_value i v by auto
    hence dist_less_e : "dist y x  e"
      by (simp add: dist_norm)
    thus ?thesis
      using y_pref_x dist_less_e y_in by blast
  qed
qed

end