Theory ZFC_in_HOL.Kirby

section ‹Addition and Multiplication of Sets›

theory Kirby
  imports ZFC_Cardinals

begin

subsection ‹Generalised Addition›

text ‹Source: Laurence Kirby, Addition and multiplication of sets
      Math. Log. Quart. 53, No. 1, 52-65 (2007) / DOI 10.1002/malq.200610026
      @{url "http://faculty.baruch.cuny.edu/lkirby/mlqarticlejan2007.pdf"}›

subsubsection ‹Addition is a monoid›

instantiation V :: plus
begin

text‹This definition is credited to Tarski›
definition plus_V :: "V ⇒ V ⇒ V"
  where "plus_V x ≡ transrec (λf z. x ⊔ set (f ` elts z))"

instance ..
end

definition lift :: "V ⇒ V ⇒ V"
  where "lift x y ≡ set (plus x ` elts y)"

lemma plus: "x + y = x ⊔ set ((+)x ` elts y)"
  unfolding plus_V_def  by (subst transrec) auto

lemma plus_eq_lift: "x + y = x ⊔ lift x y"
  unfolding lift_def  using plus by blast

text‹Lemma 3.2›
lemma lift_sup_distrib: "lift x (a ⊔ b) = lift x a ⊔ lift x b"
  by (simp add: image_Un lift_def sup_V_def)

lemma lift_Sup_distrib: "small Y ⟹ lift x (⨆ Y) = ⨆ (lift x ` Y)"
  by (auto simp: lift_def Sup_V_def image_Union)

lemma add_Sup_distrib:
  fixes x::V shows "y ≠ 0 ⟹ x + (⨆z∈elts y. f z) = (⨆z∈elts y. x + f z)"
  by (auto simp: plus_eq_lift SUP_sup_distrib lift_Sup_distrib image_image)

lemma Limit_add_Sup_distrib:
  fixes x::V shows "Limit α ⟹ x + (⨆z∈elts α. f z) = (⨆z∈elts α. x + f z)"
  using add_Sup_distrib by force

text‹Proposition 3.3(ii)›
instantiation V :: monoid_add
begin
instance
proof
  show "a + b + c = a + (b + c)" for a b c :: V
  proof (induction c rule: eps_induct)
    case (step c)
    have "(a+b) + c = a + b ⊔ set ((+) (a + b) ` elts c)"
      by (metis plus)
    also have "… = a ⊔ lift a b ⊔ set ((λu. a + (b+u)) ` elts c)"
      using plus_eq_lift step.IH by auto
    also have "… = a ⊔ lift a (b + c)"
    proof -
      have "lift a b ⊔ set ((λu. a + (b + u)) ` elts c) = lift a (b + c)"
        unfolding lift_def
        by (metis elts_of_set image_image lift_def lift_sup_distrib plus_eq_lift replacement small_elts)
      then show ?thesis
        by (simp add: sup_assoc)
    qed
    also have "… = a + (b + c)"
      using plus_eq_lift by auto
    finally show ?case .
  qed
  show "0 + x = x" for x :: V
  proof (induction rule: eps_induct)
    case (step x)
    then show ?case
      by (subst plus) auto
  qed
  show "x + 0 = x" for x :: V
    by (subst plus) auto
qed
end

lemma lift_0 [simp]: "lift 0 x = x"
  by (simp add: lift_def)

lemma lift_by0 [simp]: "lift x 0 = 0"
  by (simp add: lift_def)

lemma lift_by1 [simp]: "lift x 1 = set{x}"
  by (simp add: lift_def)

lemma add_eq_0_iff [simp]:
  fixes x y::V
  shows "x+y = 0 ⟷ x=0 ∧ y=0"
  proof safe
  show "x = 0" if "x + y = 0"
    by (metis that le_imp_less_or_eq not_less_0 plus sup_ge1)
  then show "y = 0" if "x + y = 0"
    using that by auto
qed auto

lemma plus_vinsert: "x + vinsert z y = vinsert (x+z) (x + y)"
proof -
  have f1: "elts (x + y) = elts x ∪ (+) x ` elts y"
    by (metis elts_of_set lift_def plus_eq_lift replacement small_Un small_elts sup_V_def)
  moreover have "lift x (vinsert z y) = set ((+) x ` elts (set (insert z (elts y))))"
    using vinsert_def lift_def by presburger
  ultimately show ?thesis
    by (simp add: vinsert_def plus_eq_lift sup_V_def)
qed

lemma plus_V_succ_right: "x + succ y = succ (x + y)"
  by (metis plus_vinsert succ_def)

lemma succ_eq_add1: "succ x = x + 1"
  by (simp add: plus_V_succ_right one_V_def)

lemma ord_of_nat_add: "ord_of_nat (m+n) = ord_of_nat m + ord_of_nat n"
  by (induction n) (auto simp: plus_V_succ_right)

lemma succ_0_plus_eq [simp]:
  assumes "α ∈ elts ω" 
  shows "succ 0 + α = succ α"
proof -
  obtain n where "α = ord_of_nat n"
    using assms elts_ω by blast
  then show ?thesis
    by (metis One_nat_def ord_of_nat.simps ord_of_nat_add plus_1_eq_Suc)
qed

lemma omega_closed_add [intro]:
  assumes "α ∈ elts ω" "β ∈ elts ω" shows "α+β ∈ elts ω"
proof -
  obtain m n where "α = ord_of_nat m" "β = ord_of_nat n"
    using assms elts_ω by auto
  then have "α+β = ord_of_nat (m+n)"
    using ord_of_nat_add by auto
  then show ?thesis
    by (simp add: ω_def)
qed

lemma mem_plus_V_E:
  assumes l: "l ∈ elts (x + y)"
  obtains "l ∈ elts x" | z where "z ∈ elts y" "l = x + z"
  using l by (auto simp: plus [of x y] split: if_split_asm)

lemma not_add_less_right: assumes "Ord y" shows "¬ (x + y < x)"
  using assms
proof (induction rule: Ord_induct)
  case (step i)
  then show ?case
    by (metis less_le_not_le plus sup_ge1)
qed

lemma not_add_mem_right: "¬ (x + y ∈ elts x)"
  by (metis sup_ge1 mem_not_refl plus vsubsetD)

text‹Proposition 3.3(iii)›
lemma add_not_less_TC_self: "¬ x + y ⊏ x"
proof (induction y arbitrary: x rule: eps_induct)
  case (step y)
  then show ?case
    using less_TC_imp_not_le plus_eq_lift by fastforce
qed

lemma TC_sup_lift: "TC x ⊓ lift x y = 0"
proof -
  have "elts (TC x) ∩ elts (set ((+) x ` elts y)) = {}"
    using add_not_less_TC_self by (auto simp: less_TC_def)
  then have "TC x ⊓ set ((+) x ` elts y) = set {}"
    by (metis inf_V_def)
  then show ?thesis
    using lift_def by auto
qed

lemma lift_lift: "lift x (lift y z) = lift (x+y) z"
  using add.assoc  by (auto simp: lift_def)

lemma lift_self_disjoint: "x ⊓ lift x u = 0"
  by (metis TC_sup_lift arg_subset_TC inf.absorb_iff2 inf_assoc inf_sup_aci(3) lift_0)

lemma sup_lift_eq_lift:
  assumes "x ⊔ lift x u = x ⊔ lift x v"
  shows "lift x u = lift x v"
  by (metis (no_types) assms inf_sup_absorb inf_sup_distrib2 lift_self_disjoint sup_commute sup_inf_absorb)

subsubsection ‹Deeper properties of addition›

text‹Proposition 3.4(i)›
proposition lift_eq_lift: "lift x y = lift x z ⟹ y = z"
proof (induction y arbitrary: z rule: eps_induct)
  case (step y)
  show ?case
  proof (intro vsubsetI order_antisym)
    show "u ∈ elts z" if "u ∈ elts y" for u
    proof -
      have "x+u ∈ elts (lift x z)"
        using lift_def step.prems that by fastforce
      then obtain v where "v ∈ elts z" "x+u = x+v"
        using lift_def by auto
      then have "lift x u = lift x v"
        using sup_lift_eq_lift by (simp add: plus_eq_lift)
      then have "u=v"
        using step.IH that by blast
      then show ?thesis
        using ‹v ∈ elts z› by blast
    qed
    show "u ∈ elts y" if "u ∈ elts z" for u
    proof -
      have "x+u ∈ elts (lift x y)"
        using lift_def step.prems that by fastforce
      then obtain v where "v ∈ elts y" "x+u = x+v"
        using lift_def by auto
      then have "lift x u = lift x v"
        using sup_lift_eq_lift by (simp add: plus_eq_lift)
      then have "u=v"
        using step.IH by (metis ‹v ∈ elts y›)
      then show ?thesis
        using ‹v ∈ elts y› by auto
    qed
  qed
qed

corollary inj_lift: "inj_on (lift x) A"
  by (auto simp: inj_on_def dest: lift_eq_lift)

corollary add_right_cancel [iff]:
  fixes x y z::V shows "x+y = x+z ⟷ y=z"
  by (metis lift_eq_lift plus_eq_lift sup_lift_eq_lift)

corollary add_mem_right_cancel [iff]:
  fixes x y z::V shows "x+y ∈ elts (x+z) ⟷ y ∈ elts z"
  apply safe
   apply (metis mem_plus_V_E not_add_mem_right add_right_cancel)
  by (metis ZFC_in_HOL.ext dual_order.antisym elts_vinsert insert_subset order_refl plus_vinsert)

corollary add_le_cancel_left [iff]:
  fixes x y z::V shows "x+y ≤ x+z ⟷ y≤z"
  by auto (metis add_mem_right_cancel mem_plus_V_E plus sup_ge1 vsubsetD)

corollary add_less_cancel_left [iff]:
  fixes x y z::V shows "x+y < x+z ⟷ y<z"
  by (simp add: less_le_not_le)

corollary lift_le_self [simp]: "lift x y ≤ x ⟷ y = 0"
  by (auto simp: inf.absorb_iff2 lift_eq_lift lift_self_disjoint)

lemma succ_less_ω_imp: "succ x < ω ⟹ x < ω"
  by (metis add_le_cancel_left add.right_neutral le_0 le_less_trans succ_eq_add1)

text‹Proposition 3.5›
lemma card_lift: "vcard (lift x y) = vcard y"
proof (rule cardinal_cong)
  have "bij_betw ((+)x) (elts y) (elts (lift x y))"
    unfolding bij_betw_def
    by (simp add: inj_on_def lift_def)
  then show "elts (lift x y) ≈ elts y"
    using eqpoll_def eqpoll_sym by blast
qed

lemma eqpoll_lift: "elts (lift x y) ≈ elts y"
  by (metis card_lift cardinal_eqpoll eqpoll_sym eqpoll_trans)

lemma vcard_add: "vcard (x + y) = vcard x ⊕ vcard y"
  using card_lift [of x y] lift_self_disjoint [of x]
  by (simp add: plus_eq_lift vcard_disjoint_sup)

lemma countable_add:
  assumes "countable (elts A)" "countable (elts B)"
  shows "countable (elts (A+B))"
proof -
  have "vcard A ≤ ℵ0" "vcard B ≤ ℵ0"
    using assms countable_iff_le_Aleph0 by blast+
  then have "vcard (A+B) ≤ ℵ0"
    unfolding vcard_add
    by (metis Aleph_0 Card_ω InfCard_cdouble_eq InfCard_def cadd_le_mono order_refl)
  then show ?thesis
    by (simp add: countable_iff_le_Aleph0)
qed

text‹Proposition 3.6›
proposition TC_add: "TC (x + y) = TC x ⊔ lift x (TC y)"
proof (induction y rule: eps_induct)
  case (step y)
  have *: "⨆ (TC ` (+) x ` elts y) = TC x ⊔ (⨆u∈elts y. TC (set ((+) x ` elts u)))"
    if "elts y ≠ {}"
  proof -
    obtain w where "w ∈ elts y"
      using ‹elts y ≠ {}› by blast
    then have "TC x ≤ TC (x + w)"
      by (simp add: step.IH)
    then have †: "TC x ≤ (⨆w∈elts y. TC (x + w))"
      using ‹w ∈ elts y› by blast
    show ?thesis
      using that
      apply (intro conjI ballI impI order_antisym; clarsimp simp add: image_comp †)
       apply(metis TC_sup_distrib Un_iff elts_sup_iff plus)
      by (metis TC_least Transset_TC arg_subset_TC le_sup_iff plus vsubsetD)
  qed
  have "TC (x + y) = (x + y) ⊔ ⨆ (TC ` elts (x + y))"
    using TC by blast
  also have "… = x ⊔ lift x y ⊔ ⨆ (TC ` elts x) ⊔ ⨆ ((λu. TC (x+u)) ` elts y)"
    apply (simp add: plus_eq_lift image_Un Sup_Un_distrib sup.left_commute sup_assoc TC_sup_distrib SUP_sup_distrib)
    apply (simp add: lift_def sup.commute sup_aci *)
    done
  also have "… = x ⊔ ⨆ (TC ` elts x) ⊔ lift x y ⊔ ⨆ ((λu. TC x ⊔ lift x (TC u)) ` elts y)"
    by (simp add: sup_aci step.IH)
  also have "… = TC x ⊔ lift x y ⊔ ⨆ ((λu. lift x (TC u)) ` elts y)"
    by (simp add: sup_aci SUP_sup_distrib flip: TC [of x])
  also have "… = TC x ⊔ lift x (y ⊔ ⨆ (TC ` elts y))"
    by (metis (no_types) elts_of_set lift_Sup_distrib image_image lift_sup_distrib replacement small_elts sup_assoc)
  also have "… = TC x ⊔ lift x (TC y)"
    by (simp add: TC [of y])
  finally show ?case .
qed

corollary TC_add': "z ⊏ x + y ⟷ z ⊏ x ∨ (∃v. v ⊏ y ∧ z = x + v)"
  using TC_add by (force simp: less_TC_def lift_def)

text‹Corollary 3.7›
corollary vcard_TC_add: "vcard (TC (x+y)) = vcard (TC x) ⊕ vcard (TC y)"
  by (simp add: TC_add TC_sup_lift card_lift vcard_disjoint_sup)

text‹Corollary 3.8›
corollary TC_lift:
  assumes "y ≠ 0"
  shows "TC (lift x y) = TC x ⊔ lift x (TC y)"
proof -
  have "TC (lift x y) = lift x y ⊔ ⨆ ((λu. TC(x+u)) ` elts y)"
    unfolding TC [of "lift x y"]  by (simp add: lift_def image_image)
  also have "… = lift x y ⊔ (⨆u∈elts y. TC x ⊔ lift x (TC u))"
    by (simp add: TC_add)
  also have "… = lift x y ⊔ TC x ⊔ (⨆u∈elts y. lift x (TC u))"
    using assms by (auto simp: SUP_sup_distrib)
  also have "… = TC x ⊔ lift x (TC y)"
    by (simp add: TC [of y] sup_aci image_image lift_sup_distrib lift_Sup_distrib)
  finally show ?thesis .
qed

proposition rank_add_distrib: "rank (x+y) = rank x + rank y"
proof (induction y rule: eps_induct)
  case (step y)
  show ?case
  proof (cases "y=0")
    case False
    then obtain e where e: "e ∈ elts y"
      by fastforce
    have "rank (x+y) = (⨆u∈elts (x ⊔ ZFC_in_HOL.set ((+) x ` elts y)). succ (rank u))"
      by (metis plus rank_Sup)
    also have "… = (⨆x∈elts x. succ (rank x)) ⊔ (⨆z∈elts y. succ (rank x + rank z))"
      apply (simp add: Sup_Un_distrib image_Un image_image)
      apply (simp add: step cong: SUP_cong_simp)
      done
    also have "… = (⨆z ∈ elts y. rank x + succ (rank z))"
    proof -
      have "rank x ≤ (⨆z∈elts y. ZFC_in_HOL.succ (rank x + rank z))"
        using ‹y ≠ 0›
        by (auto simp: plus_eq_lift intro: order_trans [OF _ cSUP_upper [OF e]])
      then show ?thesis
        by (force simp: plus_V_succ_right simp flip: rank_Sup [of x] intro!: order_antisym)
    qed
    also have "… = rank x + (⨆z ∈ elts y. succ (rank z))"
      by (simp add: add_Sup_distrib False)
    also have "… = rank x + rank y"
      by (simp add: rank_Sup [of y])
    finally show ?thesis .
  qed auto
qed

lemma Ord_add [simp]: "⟦Ord x; Ord y⟧ ⟹ Ord (x+y)"
proof (induction y rule: eps_induct)
  case (step y)
  then show ?case
    by (metis Ord_rank rank_add_distrib rank_of_Ord)
qed

lemma add_Sup_distrib_id: "A ≠ 0 ⟹ x + ⨆(elts A) = (⨆z∈elts A. x + z)"
  by (metis add_Sup_distrib image_ident image_image)

lemma add_Limit: "Limit α ⟹ x + α = (⨆z∈elts α. x + z)"
  by (metis Limit_add_Sup_distrib Limit_eq_Sup_self image_ident image_image)

lemma add_le_left:
  assumes "Ord α" "Ord β" shows "β ≤ α+β"
  using ‹Ord β›
proof (induction rule: Ord_induct3)
  case 0
  then show ?case
    by auto
next
  case (succ α)
  then show ?case
    by (auto simp: plus_V_succ_right Ord_mem_iff_lt assms(1))
next
  case (Limit μ)
  then have k: "μ = (⨆β ∈ elts μ. β)"
    by (simp add: Limit_eq_Sup_self)
  also have "…  ≤ (⨆β ∈ elts μ. α + β)"
    using Limit.IH by auto
  also have "… = α + (⨆β ∈ elts μ. β)"
    using Limit.hyps Limit_add_Sup_distrib by presburger
  finally show ?case
    using k by simp
qed

lemma plus_ω_equals_ω:
  assumes "α ∈ elts ω"  shows "α + ω = ω"
proof (rule antisym)
  show "α + ω ≤ ω"
    using Ord_trans assms by (auto simp: elim!: mem_plus_V_E)
  show "ω ≤ α + ω"
    by (simp add: add_le_left assms)
qed

lemma one_plus_ω_equals_ω [simp]: "1 + ω = ω"
  by (simp add: one_V_def plus_ω_equals_ω)

subsubsection ‹Cancellation / set subtraction›

definition vle :: "V ⇒ V ⇒ bool" (infix ‹⊴› 50)
  where "x ⊴ y ≡ ∃z::V. x+z = y"

lemma vle_refl [iff]: "x ⊴ x"
  by (metis (no_types) add.right_neutral vle_def)

lemma vle_antisym: "⟦x ⊴ y; y ⊴ x⟧ ⟹ x = y"
  by (metis V_equalityI plus_eq_lift sup_ge1 vle_def vsubsetD)

lemma vle_trans [trans]: "⟦x ⊴ y; y ⊴ z⟧ ⟹ x ⊴ z"
  by (metis add.assoc vle_def)

definition vle_comparable :: "V ⇒ V ⇒ bool"
  where "vle_comparable x y ≡ x ⊴ y ∨ y ⊴ x"

text‹Lemma 3.13›
lemma comparable:
  assumes "a+b = c+d"
  shows "vle_comparable a c"
unfolding vle_comparable_def
proof (rule ccontr)
  assume non: "¬ (a ⊴ c ∨ c ⊴ a)"
  let ?φ = "λx. ∀z. a+x ≠ c+z"
  have "?φ x" for x
  proof (induction x rule: eps_induct)
    case (step x)
    show ?case
    proof (cases "x=0")
      case True
      with non nonzero_less_TC show ?thesis
        using vle_def by auto
    next
      case False
      then obtain v where "v ∈ elts x"
        using trad_foundation by blast
      show ?thesis
      proof clarsimp
        fix z
        assume eq: "a + x = c + z"
        then have "z ≠ 0"
          using vle_def non by auto
        have av: "a+v ∈ elts (a+x)"
          by (simp add: ‹v ∈ elts x›)
        moreover have "a+x = c ⊔ lift c z"
          using eq plus_eq_lift by fastforce
        ultimately have "a+v ∈ elts (c ⊔ lift c z)"
          by simp
        moreover
        define u where "u ≡ set (elts x - {v})"
        have u: "v ∉ elts u" and xeq: "x = vinsert v u"
          using ‹v ∈ elts x› by (auto simp: u_def intro: order_antisym)
        have case1: "a+v ∉ elts c"
        proof
          assume avc: "a + v ∈ elts c"
          then have "a ≤ c"
            by clarify (metis Un_iff elts_sup_iff eq mem_not_sym mem_plus_V_E plus_eq_lift)
          moreover have "a ⊔ lift a x = c ⊔ lift c z"
            using eq by (simp add: plus_eq_lift)
          ultimately have "lift c z ≤ lift a x"
            by (metis inf.absorb_iff2 inf_commute inf_sup_absorb inf_sup_distrib2 lift_self_disjoint sup.commute)
          also have "… = vinsert (a+v) (lift a u)"
            by (simp add: lift_def vinsert_def xeq)
          finally have *: "lift c z ≤ vinsert (a + v) (lift a u)" .
          have "lift c z ≤ lift a u"
          proof -
            have "a + v ∉ elts (lift c z)"
              using lift_self_disjoint [of c z] avc V_disjoint_iff by auto
            then show ?thesis
              using * less_eq_V_def by auto
          qed
          { fix e
            assume "e ∈ elts z"
            then have "c+e ∈ elts (lift c z)"
              by (simp add: lift_def)
            then have "c+e ∈ elts (lift a u)"
              using ‹lift c z ≤ lift a u› by blast
            then obtain y where "y ∈ elts u" "c+e = a+y"
              using lift_def by auto
            then have False
              by (metis elts_vinsert insert_iff step.IH xeq)
          }
          then show False
            using ‹z ≠ 0› by fastforce
        qed
        ultimately show False
          by (metis (no_types) ‹v ∈ elts x› av case1 eq mem_plus_V_E step.IH)
      qed
    qed
  qed
  then show False
    using assms by blast
qed

lemma vle1: "x ⊴ y ⟹ x ≤ y"
  using vle_def plus_eq_lift by auto

lemma vle2: "x ⊴ y ⟹ x ⊑ y"
  by (metis (full_types) TC_add' add.right_neutral le_TC_def vle_def nonzero_less_TC)

lemma vle_iff_le_Ord:
  assumes "Ord α" "Ord β"
  shows "α ⊴ β ⟷ α ≤ β"
proof
  show "α ≤ β" if "α ⊴ β"
    using that by (simp add: vle1)
  show "α ⊴ β" if "α ≤ β"
    using ‹Ord α› ‹Ord β› that
  proof (induction α arbitrary: β rule: Ord_induct)
    case (step γ)
    then show ?case
      unfolding vle_def
      by (metis Ord_add Ord_linear add_le_left mem_not_refl mem_plus_V_E vsubsetD)
  qed
qed

lemma add_le_cancel_left0 [iff]:
  fixes x::V shows "x ≤ x+z"
  by (simp add: vle1 vle_def)

lemma add_less_cancel_left0 [iff]:
  fixes x::V shows "x < x+z ⟷ 0<z"
  by (metis add_less_cancel_left add.right_neutral)

lemma le_Ord_diff:
  assumes "α ≤ β" "Ord α" "Ord β"
  obtains γ where "α+γ = β" "γ ≤ β" "Ord γ"
proof -
  obtain γ where γ: "α+γ = β" "γ ≤ β"
    by (metis add_le_cancel_left add_le_left assms vle_def vle_iff_le_Ord)
  then have "Ord γ"
    using Ord_def Transset_def ‹Ord β› by force
  with γ that show thesis by blast
qed

lemma plus_Ord_le:
  assumes "α ∈ elts ω" "Ord β" shows "α+β ≤ β+α"
proof (cases "β ∈ elts ω")
  case True
  with assms have "α+β = β+α"
    by (auto simp: elts_ω add.commute ord_of_nat_add [symmetric])
  then show ?thesis by simp
next
  case False
  then have "ω ≤ β" 
    using Ord_linear2 Ord_mem_iff_lt ‹Ord β› by auto
  then obtain γ where "ω+γ = β" "γ ≤ β" "Ord γ"
    using ‹Ord β› le_Ord_diff by auto
  then have "α+β = β"
    by (metis add.assoc assms(1) plus_ω_equals_ω)
  then show ?thesis
    by simp
qed

lemma add_right_mono: "⟦α ≤ β; Ord α; Ord β; Ord γ⟧ ⟹ α+γ ≤ β+γ"
  by (metis add_le_cancel_left add.assoc add_le_left le_Ord_diff)

lemma add_strict_mono: "⟦α < β; γ < δ; Ord α; Ord β; Ord γ; Ord δ⟧ ⟹ α+γ < β+δ"
  by (metis order.strict_implies_order add_less_cancel_left add_right_mono le_less_trans)

lemma add_right_strict_mono: "⟦α ≤ β; γ < δ; Ord α; Ord β; Ord γ; Ord δ⟧ ⟹ α+γ < β+δ"
  using add_strict_mono le_imp_less_or_eq by blast

lemma Limit_add_Limit [simp]:
  assumes "Limit μ" "Ord β" shows "Limit (β + μ)"
  unfolding Limit_def
  proof (intro conjI allI impI)
  show "Ord (β + μ)"
    using Limit_def assms by auto
  show "0 ∈ elts (β + μ)"
    using Limit_def add_le_left assms by auto
next
  fix γ
  assume "γ ∈ elts (β + μ)"
  then consider "γ ∈ elts β" | ξ where "ξ ∈ elts μ" "γ = β + ξ"
    using mem_plus_V_E by blast
  then show "succ γ ∈ elts (β + μ)"
  proof cases
    case 1
    then show ?thesis
      by (metis Kirby.add_strict_mono Limit_def Ord_add Ord_in_Ord Ord_mem_iff_lt assms one_V_def succ_eq_add1)
  next
    case 2
    then show ?thesis
      by (metis Limit_def add_mem_right_cancel assms(1) plus_V_succ_right)
  qed
qed


subsection ‹Generalised Difference›

definition odiff where "odiff y x ≡ THE z::V. (x+z = y) ∨ (z=0 ∧ ¬ x ⊴ y)"

lemma vle_imp_odiff_eq: "x ⊴ y ⟹ x + (odiff y x) = y"
  by (auto simp: vle_def odiff_def)

lemma not_vle_imp_odiff_0: "¬ x ⊴ y ⟹ (odiff y x) = 0"
  by (auto simp: vle_def odiff_def)

lemma Ord_odiff_eq:
  assumes "α ≤ β" "Ord α" "Ord β"
  shows "α + odiff β α = β"
  by (simp add: assms vle_iff_le_Ord vle_imp_odiff_eq)

lemma Ord_odiff:
  assumes "Ord α" "Ord β" shows "Ord (odiff β α)"
proof (cases "α ⊴ β")
  case True
  then show ?thesis
    by (metis add_right_cancel assms le_Ord_diff vle1 vle_imp_odiff_eq)
next
  case False
  then show ?thesis
    by (simp add: odiff_def vle_def)
qed

lemma Ord_odiff_le:
  assumes  "Ord α" "Ord β" shows "odiff β α ≤ β"
proof (cases "α ⊴ β")
  case True
  then show ?thesis
    by (metis add_right_cancel assms le_Ord_diff vle1 vle_imp_odiff_eq)
next
  case False
  then show ?thesis 
    by (simp add: odiff_def vle_def)
qed


lemma odiff_0_right [simp]: "odiff x 0 = x"
  by (metis add.left_neutral vle_def vle_imp_odiff_eq)

lemma odiff_succ: "y ⊴ x ⟹ odiff (succ x) y = succ (odiff x y)"
  unfolding odiff_def
  by (metis add_right_cancel odiff_def plus_V_succ_right vle_def vle_imp_odiff_eq)

lemma odiff_eq_iff: "z ⊴ x ⟹ odiff x z = y ⟷ x = z + y"
  by (auto simp: odiff_def vle_def)

lemma odiff_le_iff: "z ⊴ x ⟹ odiff x z ≤ y ⟷ x ≤ z + y"
  by (auto simp: odiff_def vle_def)

lemma odiff_less_iff: "z ⊴ x ⟹ odiff x z < y ⟷ x < z + y"
  by (auto simp: odiff_def vle_def)

lemma odiff_ge_iff: "z ⊴ x ⟹ odiff x z ≥ y ⟷ x ≥ z + y"
  by (auto simp: odiff_def vle_def)

lemma Ord_odiff_le_iff: "⟦α ≤ x; Ord x; Ord α⟧ ⟹ odiff x α ≤ y ⟷ x ≤ α + y"
  by (simp add: odiff_le_iff vle_iff_le_Ord)

lemma odiff_le_odiff:
  assumes "x ⊴ y" shows "odiff x z ≤ odiff y z"
proof (cases "z ⊴ x")
  case True
  then show ?thesis
    using assms odiff_le_iff vle1 vle_imp_odiff_eq vle_trans by presburger
next
  case False
  then show ?thesis
    by (simp add: not_vle_imp_odiff_0)
qed

lemma Ord_odiff_le_odiff: "⟦x ≤ y; Ord x; Ord y⟧ ⟹ odiff x α ≤ odiff y α"
  by (simp add: odiff_le_odiff vle_iff_le_Ord)

lemma Ord_odiff_less_odiff: "⟦α ≤ x; x < y; Ord x; Ord y; Ord α⟧ ⟹ odiff x α < odiff y α"
  by (metis Ord_odiff_eq Ord_odiff_le_odiff dual_order.strict_trans less_V_def)

lemma Ord_odiff_less_imp_less: "⟦odiff x α < odiff y α; Ord x; Ord y⟧ ⟹ x < y"
  by (meson Ord_linear2 leD odiff_le_odiff vle_iff_le_Ord)

lemma odiff_add_cancel [simp]: "odiff (x + y) x = y"
  by (simp add: odiff_eq_iff vle_def)

lemma odiff_add_cancel_0 [simp]: "odiff x x = 0"
  by (simp add: odiff_eq_iff)

lemma odiff_add_cancel_both [simp]: "odiff (x + y) (x + z) = odiff y z"
  by (simp add: add.assoc odiff_def vle_def)


subsection ‹Generalised Multiplication›

text ‹Credited to Dana Scott›

instantiation V :: times
begin

text‹This definition is credited to Tarski›
definition times_V :: "V ⇒ V ⇒ V"
  where "times_V x ≡ transrec (λf y. ⨆ ((λu. lift (f u) x) ` elts y))"

instance ..
end

lemma mult: "x * y = (⨆u∈elts y. lift (x * u) x)"
  unfolding times_V_def  by (subst transrec) (force simp:)

lemma elts_multE:
  assumes "z ∈ elts (x * y)" 
  obtains u v where "u ∈ elts x" "v ∈ elts y" "z = x*v + u" 
  using mult [of x y] lift_def assms by auto

text ‹Lemma 4.2›

lemma mult_zero_right [simp]:
  fixes x::V shows "x * 0 = 0"
  by (metis ZFC_in_HOL.Sup_empty elts_0 image_empty mult)

lemma mult_insert: "x * (vinsert y z) = x*z ⊔ lift (x*y) x"
  by (metis (no_types, lifting) elts_vinsert image_insert replacement small_elts sup_commute mult Sup_V_insert)

lemma mult_succ: "x * succ y = x*y + x"
  by (simp add: mult_insert plus_eq_lift succ_def)

lemma ord_of_nat_mult: "ord_of_nat (m*n) = ord_of_nat m * ord_of_nat n"
proof (induction n)
  case (Suc n)
  then show ?case
    by (simp add: add.commute [of m]) (simp add: ord_of_nat_add mult_succ)
qed auto

lemma omega_closed_mult [intro]:
  assumes "α ∈ elts ω" "β ∈ elts ω" shows "α*β ∈ elts ω"
proof -
  obtain m n where "α = ord_of_nat m" "β = ord_of_nat n"
    using assms elts_ω by auto
  then have "α*β = ord_of_nat (m*n)"
    by (simp add: ord_of_nat_mult)
  then show ?thesis
    by (simp add: ω_def)
qed

lemma zero_imp_le_mult: "0 ∈ elts y ⟹ x ≤ x*y"
  by (auto simp: mult [of x y])
  
subsubsection‹Proposition 4.3›

lemma mult_zero_left [simp]:
  fixes x::V shows "0 * x = 0"
proof (induction x rule: eps_induct)
  case (step x)
  then show ?case
    by (subst mult) auto
qed

lemma mult_sup_distrib:
  fixes x::V shows "x * (y ⊔ z) = x*y ⊔ x*z"
  unfolding mult [of x "y ⊔ z"] mult [of x y] mult [of x z]
  by (simp add: Sup_Un_distrib image_Un)

lemma mult_Sup_distrib: "small Y ⟹ x * (⨆Y) = ⨆ ((*) x ` Y)" for Y:: "V set"
  unfolding mult [of x "⨆Y"]
  by (simp add: cSUP_UNION) (metis mult)

lemma mult_lift_imp_distrib: "x * (lift y z) = lift (x*y) (x*z) ⟹ x * (y+z) = x*y + x*z"
  by (simp add: mult_sup_distrib plus_eq_lift)

lemma mult_lift: "x * (lift y z) = lift (x*y) (x*z)"
proof (induction z rule: eps_induct)
  case (step z)
  have "x * lift y z = (⨆u∈elts (lift y z). lift (x * u) x)"
    using mult by blast
  also have "… = (⨆v∈elts z. lift (x * (y + v)) x)"
    using lift_def by auto
  also have "… = (⨆v∈elts z. lift (x * y + x * v) x)"
    using mult_lift_imp_distrib step.IH by auto
  also have "… = (⨆v∈elts z. lift (x * y) (lift (x * v) x))"
    by (simp add: lift_lift)
  also have "… = lift (x * y) (⨆v∈elts z. lift (x * v) x)"
    by (simp add: image_image lift_Sup_distrib)
  also have "… = lift (x*y) (x*z)"
    by (metis mult)
  finally show ?case .
qed

lemma mult_Limit: "Limit γ ⟹ x * γ = ⨆ ((*) x ` elts γ)"
  by (metis Limit_eq_Sup_self mult_Sup_distrib small_elts)

lemma add_mult_distrib: "x * (y+z) = x*y + x*z" for x::V
  by (simp add: mult_lift mult_lift_imp_distrib)

instantiation V :: monoid_mult
begin
instance
proof
  show "1 * x = x" for x :: V
  proof (induction x rule: eps_induct)
    case (step x)
    then show ?case
      by (subst mult) auto
  qed
  show "x * 1 = x" for x :: V
    by (subst mult) auto
  show "(x * y) * z = x * (y * z)" for x y z::V
  proof (induction z rule: eps_induct)
    case (step z)
    have "(x * y) * z = (⨆u∈elts z. lift (x * y * u) (x * y))"
      using mult by blast
    also have "… = (⨆u∈elts z. lift (x * (y * u)) (x * y))"
      using step.IH by auto
    also have "… = (⨆u∈elts z. x * lift (y * u) y)"
      using mult_lift by auto
    also have "… = x * (⨆u∈elts z. lift (y * u) y)"
      by (simp add: image_image mult_Sup_distrib)
    also have "… = x * (y * z)"
      by (metis mult)
    finally show ?case .
  qed
qed

end

lemma le_mult:
  assumes "Ord β" "β ≠ 0" shows "α ≤ α * β"
  using assms
proof (induction rule: Ord_induct3)
  case (succ α)
  then show ?case
    using mult_insert succ_def by fastforce
next
  case (Limit μ)
  have "α ∈ (*) α ` elts μ"
    using Limit.hyps Limit_def one_V_def by (metis imageI mult.right_neutral)
  then have "α ≤ ⨆ ((*) α ` elts μ)"
    by auto
  then show ?case
    by (simp add: Limit.hyps mult_Limit)
qed auto

lemma mult_sing_1 [simp]:
  fixes x::V shows "x * set{1} = lift x x"
  by (subst mult) auto

lemma mult_2_right [simp]:
  fixes x::V shows "x * set{0,1} = x+x"
  by (subst mult) (auto simp: Sup_V_insert plus_eq_lift)

lemma Ord_mult [simp]: "⟦Ord y; Ord x⟧ ⟹ Ord (x*y)"
proof (induction y rule: Ord_induct3)
  case 0
  then show ?case
    by auto
next
  case (succ k)
  then show ?case
    by (simp add: mult_succ)
next
  case (Limit k)
  then have "Ord (x * ⨆ (elts k))"
    by (metis Ord_Sup imageE mult_Sup_distrib small_elts)
  then show ?case
    using Limit.hyps Limit_eq_Sup_self by auto
qed


subsubsection ‹Proposition 4.4-5›
proposition rank_mult_distrib: "rank (x*y) = rank x * rank y"
proof (induction y rule: eps_induct)
  case (step y)
  have "rank (x*y) = (⨆y∈elts (⨆u∈elts y. lift (x * u) x). succ (rank y))"
    by (metis rank_Sup mult)
  also have "… = (⨆u∈elts y. ⨆r∈elts x. succ (rank (x * u + r)))"
    apply (simp add: lift_def image_image image_UN)
    apply (simp add: Sup_V_def)
    done
  also have "… = (⨆u∈elts y. ⨆r∈elts x. succ (rank (x * u) + rank r))"
    using rank_add_distrib by auto
  also have "… = (⨆u∈elts y. ⨆r∈elts x. succ (rank x * rank u + rank r))"
    using step arg_cong [where f = Sup] by auto
  also have "… = (⨆u∈elts y. rank x * rank u + rank x)"
  proof (rule SUP_cong)
    show "(⨆r∈elts x. succ (rank x * rank u + rank r)) = rank x * rank u + rank x"
      if "u ∈ elts y" for u
    proof (cases "x=0")
      case False
      have "(⨆r∈elts x. succ (rank x * rank u + rank r)) = rank x * rank u + (⨆y∈elts x. succ (rank y))"
      proof (rule order_antisym)
        show "(⨆r∈elts x. succ (rank x * rank u + rank r)) ≤ rank x * rank u + (⨆y∈elts x. succ (rank y))"
          by (auto simp: Sup_le_iff simp flip: plus_V_succ_right)
        have "rank x * rank u + (⨆y∈elts x. succ (rank y)) = (⨆y∈elts x. rank x * rank u + succ (rank y))"
          by (simp add: add_Sup_distrib False)
        also have "… ≤ (⨆r∈elts x. succ (rank x * rank u + rank r))"
          using plus_V_succ_right by auto
        finally show "rank x * rank u + (⨆y∈elts x. succ (rank y)) ≤ (⨆r∈elts x. succ (rank x * rank u + rank r))" .
      qed
      also have "… = rank x * rank u + rank x"
        by (metis rank_Sup)
      finally show ?thesis .
    qed auto
  qed auto
  also have "… = rank x * rank y"
    by (simp add: rank_Sup [of y] mult_Sup_distrib mult_succ image_image)
  finally show ?case .
qed

lemma mult_le1:
  fixes y::V assumes "y ≠ 0" shows "x ⊑ x * y"
proof (cases "x = 0")
  case False
  then obtain r where r: "r ∈ elts x"
    by fastforce
  from ‹y ≠ 0› show ?thesis
  proof (induction y rule: eps_induct)
    case (step y)
    show ?case
    proof (cases "y = 1")
      case False
      with ‹y ≠ 0› obtain p where p: "p ∈ elts y" "p ≠ 0"
        by (metis V_equalityI elts_1 insertI1 singletonD trad_foundation)
      then have "x*p + r ∈ elts (lift (x*p) x)"
        by (simp add: lift_def r)
      moreover have "lift (x*p) x ≤ x*y"
        by (metis bdd_above_iff_small cSUP_upper2 order_refl ‹p ∈ elts y› replacement small_elts mult)
      ultimately have "x*p + r ∈ elts (x*y)"
        by blast
      moreover have "x*p ⊑ x*p + r"
        by (metis TC_add' V_equalityI add.right_neutral eps_induct le_TC_refl less_TC_iff less_imp_le_TC)
      ultimately show ?thesis
        using step.IH [OF p] le_TC_trans less_TC_iff by blast
    qed auto
  qed
qed auto

lemma mult_eq_0_iff [simp]:
  fixes y::V shows "x * y = 0 ⟷ x=0 ∨ y=0"
proof
  show "x = 0 ∨ y = 0" if "x * y = 0"
    by (metis le_0 le_TC_def less_TC_imp_not_le mult_le1 that)
qed auto

lemma lift_lemma:
  assumes "x ≠ 0" "y ≠ 0"  shows "¬ lift (x * y) x ≤ x"
  using assms mult_le1 [of concl: x y]
  by (auto simp: le_TC_def TC_lift less_TC_def less_TC_imp_not_le)

lemma mult_le2:
  fixes y::V assumes "x ≠ 0" "y ≠ 0" "y ≠ 1" shows "x ⊏ x * y"
proof -
  obtain v where v: "v ∈ elts y" "v ≠ 0"
    using assms by fastforce
  have "x ≠ x * y"
    using lift_lemma [of x v]
    by (metis ‹x ≠ 0› bdd_above_iff_small cSUP_upper2 order_refl replacement small_elts mult v)
  then show ?thesis
  using assms mult_le1 [of y x]
    by (auto simp: le_TC_def)
qed

lemma elts_mult_ωE:
  assumes "x ∈ elts (y * ω)"
  obtains n where "n ≠ 0" "x ∈ elts (y * ord_of_nat n)" "⋀m. m < n ⟹ x ∉ elts (y * ord_of_nat m)"
proof -
  obtain k where k:  "k ≠ 0 ∧ x ∈ elts (y * ord_of_nat k)"
    using assms
    apply (simp add: mult_Limit elts_ω)
    by (metis mult_eq_0_iff elts_0 ex_in_conv ord_of_eq_0_iff that)
  define n where "n ≡ (LEAST k. k ≠ 0 ∧ x ∈ elts (y * ord_of_nat k))"
  show thesis
  proof
    show "n ≠ 0" "x ∈ elts (y * ord_of_nat n)"
      unfolding n_def by (metis (mono_tags, lifting) LeastI_ex k)+
    show "⋀m. m < n ⟹ x ∉ elts (y * ord_of_nat m)"
      by (metis (mono_tags, lifting) mult_eq_0_iff elts_0 empty_iff n_def not_less_Least ord_of_eq_0_iff)
  qed
qed


subsubsection‹Theorem 4.6›

theorem mult_eq_imp_0:
  assumes "a*x = a*y + b" "b ⊏ a"
  shows "b=0"
proof (cases "a=0 ∨ x=0")
  case True
  with assms show ?thesis
    by (metis add_le_cancel_left mult_eq_0_iff eq_iff le_0)
next
  case False
  then have "a≠0" "x≠0"
    by auto
  then show ?thesis
  proof (cases "y=0")
    case True
    then show ?thesis
      using assms less_asym_TC mult_le2 by force
  next
    case False
    have "b=0" if "Ord α" "x ∈ elts (Vset α)" "y ∈ elts (Vset α)" for α
      using that assms
    proof (induction α arbitrary: x y b rule: Ord_induct3)
      case 0
      then show ?case by auto
    next
      case (succ k)
      define Φ where "Φ ≡ λx y. ∃r. 0 ⊏ r ∧ r ⊏ a ∧ a*x = a*y + r"
      show ?case
      proof (rule ccontr)
        assume "b ≠ 0"
        then have "0 ⊏ b"
          by (metis nonzero_less_TC)
        then have "Φ x y"
          unfolding Φ_def using succ.prems by blast
        then obtain x' where "Φ x' y" "x' ⊑ x" and min: "⋀x''. x'' ⊏ x' ⟹ ¬ Φ x'' y"
          using less_TC_minimal [of "λx. Φ x y" x] by blast
        then obtain b' where "0 ⊏ b'" "b' ⊏ a" and eq: "a*x' = a*y + b'"
          using Φ_def by blast
        have "a*y ⊏ a*x'"
          using TC_add' ‹0 ⊏ b'› eq by auto
        then obtain p where "p ∈ elts (a * x')" "a * y ⊑ p"
          using less_TC_iff by blast
        then have "p ∉ elts (a * y)"
          using less_TC_iff less_irrefl_TC by blast
        then have "p ∈ ⋃ (elts ` (λv. lift (a * v) a) ` elts x')"
          by (metis ‹p ∈ elts (a * x')› elts_Sup replacement small_elts mult)
        then obtain u c where "u ∈ elts x'" "c ∈ elts a" "p = a*u + c"
          using lift_def by auto
        then have "p ∈ elts (lift (a*y) b')"
          using ‹p ∈ elts (a * x')› ‹p ∉ elts (a * y)› eq plus_eq_lift by auto
        then obtain d where d: "d ∈ elts b'" "p = a*y + d" "p = a*u + c"
          by (metis ‹p = a * u + c› ‹p ∈ elts (a * x')› ‹p ∉ elts (a * y)› eq mem_plus_V_E)
        have noteq: "a*y ≠ a*u"
        proof
          assume "a*y = a*u"
          then have "lift (a*y) a = lift (a*u) a"
            by metis
          also have "… ≤ a*x'"
            unfolding mult [of _ x'] using ‹u ∈ elts x'› by (auto intro: cSUP_upper)
          also have "… = a*y ⊔ lift (a*y) b'"
            by (simp add: eq plus_eq_lift)
          finally have "lift (a*y) a ≤ a*y ⊔ lift (a*y) b'" .
          then have "lift (a*y) a ≤ lift (a*y) b'"
            using add_le_cancel_left less_TC_imp_not_le plus_eq_lift ‹b' ⊏ a› by auto
          then have "a ≤ b'"
            by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib)
          then show False
            using ‹b' ⊏ a› less_TC_imp_not_le by auto
        qed
        consider "a*y ⊴ a*u" | "a*u ⊴ a*y"
          using d comparable vle_comparable_def by auto
        then show False
        proof cases
          case 1
          then obtain e where e: "a*u = a*y + e" "e ≠ 0"
            by (metis add.right_neutral noteq vle_def)
          moreover have "e + c = d"
            by (metis e add_right_cancel ‹p = a * u + c› ‹p = a * y + d› add.assoc)
          with ‹d ∈ elts b'› ‹b' ⊏ a› have "e ⊏ a"
            by (meson less_TC_iff less_TC_trans vle2 vle_def)
          ultimately show False
            ―‹contradicts minimality of @{term x'}›
            using min unfolding Φ_def by (meson ‹u ∈ elts x'› le_TC_def less_TC_iff nonzero_less_TC)
        next
          case 2
          then obtain e where e: "a*y = a*u + e" "e ≠ 0"
            by (metis add.right_neutral noteq vle_def)
          moreover have "e + d = c"
            by (metis e add_right_cancel ‹p = a * u + c› ‹p = a * y + d› add.assoc)
          with ‹d ∈ elts b'› ‹b' ⊏ a› have "e ⊏ a"
            by (metis ‹c ∈ elts a› less_TC_iff vle2 vle_def)
          ultimately have "Φ y u"
            unfolding Φ_def using nonzero_less_TC by blast
          then obtain y' where "Φ y' u" "y' ⊑ y" and min: "⋀x''. x'' ⊏ y' ⟹ ¬ Φ x'' u"
            using less_TC_minimal [of "λx. Φ x u" y] by blast
          then obtain b' where "0 ⊏ b'" "b' ⊏ a" and eq: "a*y' = a*u + b'"
            using Φ_def by blast
          have u_k: "u ∈ elts (Vset k)"
            using ‹u ∈ elts x'› ‹x' ⊑ x› succ Vset_succ_TC less_TC_iff less_le_TC_trans by blast
          have "a*u ⊏ a*y'"
            using TC_add' ‹0 ⊏ b'› eq by auto
          then obtain p where "p ∈ elts (a * y')" "a * u ⊑ p"
            using less_TC_iff by blast
          then have "p ∉ elts (a * u)"
            using less_TC_iff less_irrefl_TC by blast
          then have "p ∈ ⋃ (elts ` (λv. lift (a * v) a) ` elts y')"
            by (metis ‹p ∈ elts (a * y')› elts_Sup replacement small_elts mult)
          then obtain v c where "v ∈ elts y'" "c ∈ elts a" "p = a*v + c"
            using lift_def by auto
          then have "p ∈ elts (lift (a*u) b')"
            using ‹p ∈ elts (a * y')› ‹p ∉ elts (a * u)› eq plus_eq_lift by auto
          then obtain d where d: "d ∈ elts b'" "p = a*u + d" "p = a*v + c"
            by (metis ‹p = a * v + c› ‹p ∈ elts (a * y')› ‹p ∉ elts (a * u)› eq mem_plus_V_E)
          have v_k: "v ∈ elts (Vset k)"
            using Vset_succ_TC ‹v ∈ elts y'› ‹y' ⊑ y› less_TC_iff less_le_TC_trans succ.hyps succ.prems(2) by blast
          have noteq: "a*u ≠ a*v"
            proof
              assume "a*u = a*v"
              then have "lift (a*v) a ≤ a*y'"
                unfolding mult [of _ y'] using ‹v ∈ elts y'› by (auto intro: cSUP_upper)
              also have "… = a*u ⊔ lift (a*u) b'"
                by (simp add: eq plus_eq_lift)
              finally have "lift (a*v) a ≤ a*u ⊔ lift (a*u) b'" .
              then have "lift (a*u) a ≤ lift (a*u) b'"
                by (metis ‹a * u = a * v› le_iff_sup lift_sup_distrib sup_left_commute sup_lift_eq_lift)
              then have "a ≤ b'"
                by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib)
              then show False
                using ‹b' ⊏ a› less_TC_imp_not_le by auto
            qed
          consider "a*u ⊴ a*v" | "a*v ⊴ a*u"
            using d comparable vle_comparable_def by auto
          then show False
          proof cases
            case 1
            then obtain e where e: "a*v = a*u + e" "e ≠ 0"
              by (metis add.right_neutral noteq vle_def)
            moreover have "e + c = d"
              by (metis add_right_cancel ‹p = a * u + d› ‹p = a * v + c› add.assoc e)
            with ‹d ∈ elts b'› ‹b' ⊏ a› have "e ⊏ a"
              by (meson less_TC_iff less_TC_trans vle2 vle_def)
            ultimately show False
              using succ.IH u_k v_k by blast
          next
            case 2
            then obtain e where e: "a*u = a*v + e" "e ≠ 0"
              by (metis add.right_neutral noteq vle_def)
            moreover have "e + d = c"
              by (metis add_right_cancel add.assoc d e)
            with ‹d ∈ elts b'› ‹b' ⊏ a› have "e ⊏ a"
              by (metis ‹c ∈ elts a› less_TC_iff vle2 vle_def)
           ultimately show False
             using succ.IH u_k v_k by blast
          qed
        qed
      qed
    next
      case (Limit k)
      obtain i j where k: "i ∈ elts k" "j ∈ elts k"
        and x: "x ∈ elts (Vset i)"
        and y: "y ∈ elts (Vset j)"
        using that Limit by (auto simp: Limit_Vfrom_eq)
      show ?case
      proof (rule Limit.IH [of "i ⊔ j"])
        show "i ⊔ j ∈ elts k"
          by (meson k x y Limit.hyps Limit_def Ord_in_Ord Ord_mem_iff_lt Ord_sup union_less_iff)
        show "x ∈ elts (Vset (i ⊔ j))" "y ∈ elts (Vset (i ⊔ j))"
          using x y by (auto simp: Vfrom_sup)
      qed (use Limit.prems in auto)
    qed
    then show ?thesis
      by (metis two_in_Vset Ord_rank Ord_VsetI rank_lt)
  qed
qed

subsubsection‹Theorem 4.7›

lemma mult_cancellation_half:
  assumes "a*x + r ≤ a*y + s" "r ⊏ a" "s ⊏ a"
  shows "x ≤ y"
proof -
  have "x ≤ y" if "Ord α" "x ∈ elts (Vset α)" "y ∈ elts (Vset α)" for α
    using that assms
  proof (induction α arbitrary: x y r s rule: Ord_induct3)
    case 0
    then show ?case
      by auto
  next
    case (succ k)
    show ?case
    proof
      fix u
      assume u: "u ∈ elts x"
      have u_k: "u ∈ elts (Vset k)"
        using Vset_succ succ.hyps succ.prems(1) u by auto
      obtain r' where "r' ∈ elts a" "r ⊑ r'"
        using less_TC_iff succ.prems(4) by blast
      have "a*u + r' ∈ elts (lift (a*u) a)"
        by (simp add: ‹r' ∈ elts a› lift_def)
      also have "… ≤ elts (a*x)"
        using u by (force simp: mult [of _ x])
      also have "… ≤ elts (a*y + s)"
        using plus_eq_lift succ.prems(3) by auto
      also have "… = elts (a*y) ∪ elts (lift (a*y) s)"
        by (simp add: plus_eq_lift)
      finally have "a * u + r' ∈ elts (a * y) ∪ elts (lift (a * y) s)" .
      then show "u ∈ elts y"
      proof
        assume *: "a * u + r' ∈ elts (a * y)"
        show "u ∈ elts y"
        proof -
          obtain v e where v: "v ∈ elts y" "e ∈ elts a" "a * u + r' = a * v + e"
            using * by (auto simp: mult [of _ y] lift_def)
          then have v_k: "v ∈ elts (Vset k)"
            using Vset_succ_TC less_TC_iff succ.prems(2) by blast
          then show ?thesis
            by (metis ‹r' ∈ elts a› antisym le_TC_refl less_TC_iff order_refl succ.IH u_k v)
        qed
      next
        assume "a * u + r' ∈ elts (lift (a * y) s)"
        then obtain t where "t ∈ elts s" and t: "a * u + r' = a * y + t"
          using lift_def by auto
        have noteq: "a*y ≠ a*u"
        proof
          assume "a*y = a*u"
          then have "lift (a*y) a = lift (a*u) a"
            by metis
          also have "… ≤ a*x"
            unfolding mult [of _ x] using ‹u ∈ elts x› by (auto intro: cSUP_upper)
          also have "… ≤ a*y ⊔ lift (a*y) s"
            using ‹elts (a * x) ⊆ elts (a * y + s)› plus_eq_lift by auto
          finally have "lift (a*y) a ≤ a*y ⊔ lift (a*y) s" .
          then have "lift (a*y) a ≤ lift (a*y) s"
            using add_le_cancel_left less_TC_imp_not_le plus_eq_lift ‹s ⊏ a› by auto
          then have "a ≤ s"
            by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib)
          then show False
            using ‹s ⊏ a› less_TC_imp_not_le by auto
        qed
        consider "a * u ⊴ a * y" | "a * y ⊴ a * u"
          using t comparable vle_comparable_def by blast
        then have "False"
        proof cases
          case 1
          then obtain c where "a*y = a*u + c"
            by (metis vle_def)
          then have "c+t = r'"
            by (metis add_right_cancel add.assoc t)
          then have "c ⊏ a"
            using ‹r' ∈ elts a› less_TC_iff vle2 vle_def by force
          moreover have "c ≠ 0"
            using ‹a * y = a * u + c› noteq by auto
          ultimately show ?thesis
            using ‹a * y = a * u + c› mult_eq_imp_0 by blast
        next
          case 2
          then obtain c where "a*u = a*y + c"
            by (metis vle_def)
          then have "c+r' = t"
            by (metis add_right_cancel add.assoc t)
          then have "c ⊏ a"
            by (metis ‹t ∈ elts s› less_TC_iff less_TC_trans ‹s ⊏ a› vle2 vle_def)
          moreover have "c ≠ 0"
            using ‹a * u = a * y + c› noteq by auto
          ultimately show ?thesis
            using ‹a * u = a * y + c› mult_eq_imp_0 by blast
        qed
        then show "u ∈ elts y" ..
      qed
    qed
  next
    case (Limit k)
    obtain i j where k: "i ∈ elts k" "j ∈ elts k"
      and x: "x ∈ elts (Vset i)" and y: "y ∈ elts (Vset j)"
      using that Limit by (auto simp: Limit_Vfrom_eq)
    show ?case
    proof (rule Limit.IH [of "i ⊔ j"])
      show "i ⊔ j ∈ elts k"
        by (meson k x y Limit.hyps Limit_def Ord_in_Ord Ord_mem_iff_lt Ord_sup union_less_iff)
      show "x ∈ elts (Vset (i ⊔ j))" "y ∈ elts (Vset (i ⊔ j))"
        using x y by (auto simp: Vfrom_sup)
      show "a * x + r ≤ a * y + s"
        by (simp add: Limit.prems)
    qed (auto simp: Limit.prems)
  qed
  then show ?thesis
    by (metis two_in_Vset Ord_rank Ord_VsetI rank_lt)
qed

theorem mult_cancellation_lemma:
  assumes "a*x + r = a*y + s" "r ⊏ a" "s ⊏ a"
  shows "x=y ∧ r=s"
  by (metis assms leD less_V_def mult_cancellation_half odiff_add_cancel order_refl)

corollary mult_cancellation [simp]:
  fixes a::V
  assumes "a ≠ 0"
  shows "a*x = a*y ⟷ x=y"
  by (metis assms nonzero_less_TC mult_cancellation_lemma)

corollary mult_cancellation_less:
  assumes lt: "a*x + r < a*y + s" and "r ⊏ a" "s ⊏ a"
  obtains "x < y" | "x = y" "r < s"
proof -
  have "x ≤ y"
    by (meson assms dual_order.strict_implies_order mult_cancellation_half)
  then consider "x < y" | "x = y"
    using less_V_def by blast
  with lt that show ?thesis by blast
qed

corollary lift_mult_TC_disjoint:
  fixes x::V
  assumes "x ≠ y"
  shows "lift (a*x) (TC a) ⊓ lift (a*y) (TC a) = 0"
  apply (rule V_equalityI)
  using assms
  by (auto simp: less_TC_def inf_V_def lift_def image_iff dest: mult_cancellation_lemma)

corollary lift_mult_disjoint:
  fixes x::V
  assumes "x ≠ y"
  shows "lift (a*x) a ⊓ lift (a*y) a = 0"
proof -
  have "lift (a*x) a ⊓ lift (a*y) a ≤ lift (a*x) (TC a) ⊓ lift (a*y) (TC a)"
    by (metis TC' inf_mono lift_sup_distrib sup_ge1)
  then show ?thesis
    using assms lift_mult_TC_disjoint by auto
qed

lemma mult_add_mem:
  assumes "a*x + r ∈ elts (a*y)" "r ⊏ a"
  shows "x ∈ elts y" "r ∈ elts a"
proof -
  obtain v s where v: "a * x + r = a * v + s" "v ∈ elts y" "s ∈ elts a"
    using assms unfolding mult [of a y] lift_def by auto
  then show "x ∈ elts y"
    by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma vsubsetD)
  show "r ∈ elts a"
    by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma v(1) v(3) vsubsetD)
qed

lemma mult_add_mem_0 [simp]: "a*x ∈ elts (a*y) ⟷ x ∈ elts y ∧ 0 ∈ elts a"
  proof -
  have "x ∈ elts y"
    if "a * x ∈ elts (a * y) ∧ 0 ∈ elts a"
    using that   using mult_add_mem [of a x 0]
    using nonzero_less_TC by force
  moreover have "a * x ∈ elts (a * y)"
    if "x ∈ elts y" "0 ∈ elts a"
    using that  by (force simp: image_iff mult [of a y] lift_def)
  ultimately show ?thesis
    by (metis mult_eq_0_iff add.right_neutral mult_add_mem(2) nonzero_less_TC)
qed

lemma zero_mem_mult_iff: "0 ∈ elts (x*y) ⟷ 0 ∈ elts x ∧ 0 ∈ elts y" 
  by (metis Kirby.mult_zero_right mult_add_mem_0)

lemma zero_less_mult_iff [simp]: "0 < x*y ⟷ 0 < x ∧ 0 < y" if "Ord x" 
  using Kirby.mult_eq_0_iff ZFC_in_HOL.neq0_conv by blast

lemma mult_cancel_less_iff [simp]:
  "⟦Ord α; Ord β; Ord γ⟧ ⟹ α*β < α*γ ⟷ β < γ ∧ 0 < α"
  using mult_add_mem_0 [of α β γ]
  by (meson Ord_0 Ord_mem_iff_lt Ord_mult)

lemma mult_cancel_le_iff [simp]:
  "⟦Ord α; Ord β; Ord γ⟧ ⟹ α*β ≤ α*γ ⟷ β ≤ γ ∨ α=0"
  by (metis Ord_linear2 Ord_mult eq_iff leD mult_cancel_less_iff mult_cancellation)

lemma mult_Suc_add_less: "⟦α < γ; β < γ; Ord α; Ord β; Ord γ⟧  ⟹ γ * ord_of_nat m + α < γ * ord_of_nat (Suc m) + β"
  apply (simp add: mult_succ add.assoc)
  by (meson Ord_add Ord_linear2 le_less_trans not_add_less_right)

lemma mult_nat_less_add_less:
  assumes "m < n" "α < γ" "β < γ" and ord: "Ord α" "Ord β" "Ord γ"
    shows "γ * ord_of_nat m + α < γ * ord_of_nat n + β"
proof -
  have "Suc m ≤ n"
    using ‹m < n› by auto
  have "γ * ord_of_nat m + α < γ * ord_of_nat (Suc m) + β"
    using assms mult_Suc_add_less by blast
  also have "… ≤ γ * ord_of_nat n + β"
    using Ord_mult Ord_ord_of_nat add_right_mono ‹Suc m ≤ n› ord mult_cancel_le_iff ord_of_nat_mono_iff by presburger
  finally show ?thesis .
qed

lemma add_mult_less_add_mult:
  assumes "x < y" "x ∈ elts β" "y ∈ elts β" "μ ∈ elts α" "ν ∈ elts α" "Ord α" "Ord β"
    shows "α*x + μ < α*y + ν"
proof -
  obtain "Ord x" "Ord y"
    using Ord_in_Ord assms by blast
  then obtain δ where "0 ∈ elts δ" "y = x + δ"
    by (metis add.right_neutral ‹x < y› le_Ord_diff less_V_def mem_0_Ord)
  then show ?thesis
    apply (simp add: add_mult_distrib add.assoc)
    by (meson OrdmemD add_le_cancel_left0 ‹μ ∈ elts α› ‹Ord α› less_le_trans zero_imp_le_mult)
qed

lemma add_mult_less:
  assumes "γ ∈ elts α" "ν ∈ elts β" "Ord α" "Ord β"
    shows "α * ν + γ ∈ elts (α * β)"
proof -
  have "Ord ν" 
    using Ord_in_Ord assms by blast
  with assms show ?thesis
    by (metis Ord_mem_iff_lt Ord_succ add_mem_right_cancel mult_cancel_le_iff mult_succ succ_le_iff vsubsetD)
qed

lemma Ord_add_mult_iff:
  assumes "β ∈ elts γ" "β' ∈ elts γ" "Ord α" "Ord α'" "Ord γ"
  shows "γ * α + β ∈ elts (γ * α' + β') ⟷ α ∈ elts α' ∨ α = α' ∧ β ∈ elts β'" (is "?lhs ⟷ ?rhs")
proof
  assume L: ?lhs
  show ?rhs
  proof (cases "α ∈ elts α'")
    case False
    with assms have "α = α'"
      by (meson L Ord_linear Ord_mult Ord_trans add_mult_less not_add_mem_right)
    then show ?thesis
      using L less_V_def by auto
  qed auto
next
  assume R: ?rhs
  then show ?lhs
  proof
    assume "α ∈ elts α'"
    then obtain δ where "α' = α+δ"
      by (metis OrdmemD assms(3) assms(4) le_Ord_diff less_V_def)
    show ?lhs 
      using assms
      by (meson ‹α ∈ elts α'› add_le_cancel_left0 add_mult_less vsubsetD)
  next
    assume "α = α' ∧ β ∈ elts β'"
    then show ?lhs
      using less_V_def by auto
  qed
qed

lemma vcard_mult: "vcard (x * y) = vcard x ⊗ vcard y"
proof -
  have 1: "elts (lift (x * u) x) ≈ elts x" if "u ∈ elts y" for u
    by (metis cardinal_eqpoll eqpoll_sym eqpoll_trans card_lift)
  have 2: "pairwise (λu u'. disjnt (elts (lift (x * u) x)) (elts (lift (x * u') x)))  (elts y)"
    by (simp add: pairwise_def disjnt_def) (metis V_disjoint_iff lift_mult_disjoint)
  have "x * y = (⨆u∈elts y. lift (x * u) x)"
    using mult by blast
  then have "elts (x * y) ≈ (⋃u∈elts y. elts (lift (x * u) x))"
    by simp
  also have "… ≈ elts y × elts x"
    using Union_eqpoll_Times [OF 1 2] .
  also have "… ≈ elts x × elts y"
    by (simp add: times_commute_eqpoll)
  also have "… ≈ elts (vcard x) × elts (vcard y)"
    using cardinal_eqpoll eqpoll_sym times_eqpoll_cong by blast
  also have "… ≈ elts (vcard x ⊗ vcard y)"
    by (simp add: cmult_def elts_vcard_VSigma_eqpoll eqpoll_sym)
  finally have "elts (x * y) ≈ elts (vcard x ⊗ vcard y)" .
  then show ?thesis
    by (metis cadd_cmult_distrib cadd_def cardinal_cong cardinal_idem vsum_0_eqpoll)
qed

proposition TC_mult: "TC(x * y) = (⨆r ∈ elts (TC x). ⨆u ∈ elts (TC y). set{x * u + r})"
proof (cases "x = 0")
  case False
  have *: "TC(x * y) = (⨆u ∈ elts (TC y). lift (x * u) (TC x))" for y
  proof (induction y rule: eps_induct)
    case (step y)
    have "TC(x * y) = (⨆u ∈ elts y. TC (lift (x * u) x))"
      by (simp add: mult [of x y] TC_Sup_distrib image_image)
    also have "… = (⨆u ∈ elts y. TC(x * u) ⊔ lift (x * u) (TC x))"
      by (simp add: TC_lift False)
    also have "… = (⨆u ∈ elts y. (⨆z ∈ elts (TC u). lift (x * z) (TC x)) ⊔ lift (x * u) (TC x))"
      by (simp add: step)
    also have "… = (⨆u ∈ elts (TC y). lift (x * u) (TC x))"
      by (auto simp: TC' [of y] image_Un Sup_Un_distrib TC_Sup_distrib cSUP_UNION SUP_sup_distrib)
    finally show ?case .
  qed
  show ?thesis
    by (force simp: * lift_def)
qed auto


corollary vcard_TC_mult: "vcard (TC(x * y)) = vcard (TC x) ⊗ vcard (TC y)"
proof -
  have "(⋃u∈elts (TC x). ⋃v∈elts (TC y). {x * v + u}) = (⋃u∈elts (TC x). (λv. x * v + u) ` elts (TC y))"
    by (simp add: UNION_singleton_eq_range)
  also have "… ≈ (⋃x∈elts (TC x). elts (lift (TC y * x) (TC y)))"
  proof (rule UN_eqpoll_UN)
    show "(λv. x * v + u) ` elts (TC y) ≈ elts (lift (TC y * u) (TC y))"
      if "u ∈ elts (TC x)" for u
    proof -
      have "inj_on (λv. x * v + u) (elts (TC y))"
        by (meson inj_onI less_TC_def mult_cancellation_lemma that)
      then have "(λv. x * v + u) ` elts (TC y) ≈ elts (TC y)"
        by (rule inj_on_image_eqpoll_self)
      also have "… ≈ elts (lift (TC y * u) (TC y))"
        by (simp add: eqpoll_lift eqpoll_sym)
      finally show ?thesis .
    qed
    show "pairwise (λu ya. disjnt ((λv. x * v + u) ` elts (TC y)) ((λv. x * v + ya) ` elts (TC y))) (elts (TC x))"
      apply (auto simp: pairwise_def disjnt_def)
      using less_TC_def mult_cancellation_lemma by blast
    show "pairwise (λu ya. disjnt (elts (lift (TC y * u) (TC y))) (elts (lift (TC y * ya) (TC y)))) (elts (TC x))"
      apply (auto simp: pairwise_def disjnt_def)
      by (metis Int_iff V_disjoint_iff empty_iff lift_mult_disjoint)
  qed
  also have "… = elts (TC y * TC x)"
    by (metis elts_Sup image_image mult replacement small_elts)
  finally have "(⋃u∈elts (TC x). ⋃v∈elts (TC y). {x * v + u}) ≈ elts (TC y * TC x)" .
  then show ?thesis
    apply (subst cmult_commute)
    by (simp add: TC_mult cardinal_cong flip: vcard_mult)
qed

lemma countable_mult:
  assumes "countable (elts A)" "countable (elts B)"
  shows "countable (elts (A*B))"
proof -
  have "vcard A ≤ ℵ0" "vcard B ≤ ℵ0"
    using assms countable_iff_le_Aleph0 by blast+
  then have "vcard (A*B) ≤ ℵ0"
    unfolding vcard_mult
    by (metis InfCard_csquare_eq cmult_le_mono Aleph_0 Card_ω InfCard_def order_refl)
  then show ?thesis
    by (simp add: countable_iff_le_Aleph0)
qed

subsection ‹Ordertype properties›

lemma ordertype_image_plus:
  assumes "Ord α"
  shows "ordertype ((+) u ` elts α) VWF = α"
proof (subst ordertype_VWF_eq_iff)
    have 1: "(u + x, u + y) ∈ VWF" if "x ∈ elts α" "y ∈ elts α" "x < y" for x y
      using that
      by (meson Ord_in_Ord Ord_mem_iff_lt add_mem_right_cancel assms mem_imp_VWF)
  then have 2: "x < y"
    if "x ∈ elts α" "y ∈ elts α" "(u + x, u + y) ∈ VWF" for x y
    using that by (metis Ord_in_Ord Ord_linear_lt VWF_asym assms)
  show "∃f. bij_betw f ((+) u ` elts α) (elts α) ∧ (∀x∈(+) u ` elts α. ∀y∈(+) u ` elts α. (f x < f y) = ((x, y) ∈ VWF))"
    using 1 2 unfolding bij_betw_def inj_on_def
    by (rule_tac x="λx. odiff x u" in exI) (auto simp: image_iff)
qed (use assms in auto)

lemma ordertype_diff:
  assumes "β + δ = α" and α: "δ ∈ elts α" "Ord α"
  shows "ordertype (elts α - elts β) VWF = δ"
proof -
  have *: "elts α - elts β = ((+)β) ` elts δ"
  proof
    show "elts α - elts β ⊆ (+) β ` elts δ"
      by clarsimp (metis assms(1) image_iff mem_plus_V_E)
    show "(+) β ` elts δ ⊆ elts α - elts β"
      using assms(1) not_add_mem_right by force
  qed
  have "ordertype ((+) β ` elts δ) VWF = δ"
  proof (subst ordertype_VWF_inc_eq)
    show "elts δ ⊆ ON" "ordertype (elts δ) VWF = δ"
      using α elts_subset_ON ordertype_eq_Ord by blast+
  qed (use "*" assms elts_subset_ON in auto)
  then show ?thesis
    by (simp add: *)
qed

lemma ordertype_interval_eq:
  assumes α: "Ord α" and β: "Ord β"
  shows "ordertype ({α ..< α+β} ∩ ON) VWF = β"
proof -
  have ON: "(+) α ` elts β ⊆ ON"
    using assms Ord_add Ord_in_Ord by blast
  have "({α ..< α+β} ∩ ON) = (+) α ` elts β"
    using assms
    apply (simp add: image_def set_eq_iff)
    by (metis add_less_cancel_left Ord_add Ord_in_Ord Ord_linear2 Ord_mem_iff_lt le_Ord_diff not_add_less_right)
  moreover have "ordertype (elts β) VWF = ordertype ((+) α ` elts β) VWF"
    using ON β elts_subset_ON ordertype_VWF_inc_eq by auto
  ultimately show ?thesis
    using β by auto
qed

lemma ordertype_Times:
  assumes "small A" "small B" and r: "wf r" "trans r" "total_on A r" and s: "wf s" "trans s" "total_on B s"
  shows "ordertype (A×B) (r <*lex*> s) = ordertype B s * ordertype A r" (is "_ = ?β * ?α")
proof (subst ordertype_eq_iff)
  show "Ord (?β * ?α)"
    by (intro wf_Ord_ordertype Ord_mult r s; simp)
  define f where "f ≡ λ(x,y). ?β * ordermap A r x + (ordermap B s y)"
  show "∃f. bij_betw f (A × B) (elts (?β * ?α)) ∧ (∀x∈A × B. ∀y∈A × B. (f x < f y) = ((x, y) ∈ (r <*lex*> s)))"
    unfolding bij_betw_def
  proof (intro exI conjI strip)
    show "inj_on f (A × B)"
    proof (clarsimp simp: f_def inj_on_def)
      fix x y x' y'
      assume "x ∈ A" "y ∈ B" "x' ∈ A" "y' ∈ B"
        and eq: "?β * ordermap A r x + ordermap B s y = ?β * ordermap A r x' + ordermap B s y'"
      have "ordermap A r x = ordermap A r x' ∧
            ordermap B s y = ordermap B s y'"
      proof (rule mult_cancellation_lemma [OF eq])
        show "ordermap B s y ⊏ ?β"
          using ordermap_in_ordertype [OF ‹y ∈ B›, of s] less_TC_iff ‹small B› by blast 
        show "ordermap B s y' ⊏ ?β"
          using ordermap_in_ordertype [OF ‹y' ∈ B›, of s] less_TC_iff ‹small B› by blast 
      qed
      then show "x = x' ∧ y = y'"
        using ‹x ∈ A› ‹x' ∈ A› ‹y ∈ B› ‹y' ∈ B› r s ‹small A› ‹small B› by auto
    qed
    show "f ` (A × B) = elts (?β * ?α)" (is "?lhs = ?rhs")
    proof 
      show "f ` (A × B) ⊆ elts (?β * ?α)"
        apply (auto simp: f_def add_mult_less ordermap_in_ordertype wf_Ord_ordertype r s)
        by (simp add: add_mult_less assms ordermap_in_ordertype wf_Ord_ordertype)
      show "elts (?β * ?α) ⊆ f ` (A × B)"
      proof (clarsimp simp: f_def image_iff elim !: elts_multE split: prod.split)
        fix u v
        assume u: "u ∈ elts (?β)" and v: "v ∈ elts ?α"
        have "inv_into B (ordermap B s) u ∈ B"
          by (simp add: inv_into_ordermap u)
        moreover have "inv_into A (ordermap A r) v ∈ A"
          by (simp add: inv_into_ordermap v)
        ultimately show "∃x∈A. ∃y∈B. ?β * v + u = ?β * ordermap A r x + ordermap B s y"
          by (metis ‹small A› ‹small B› bij_betw_inv_into_right ordermap_bij r(1) r(3) s(1) s(3) u v)
      qed
    qed
  next
    fix p q
    assume "p ∈ A × B" and "q ∈ A × B"
    then obtain u v x y where §: "p = (u,v)" "u ∈ A" "v ∈ B" "q = (x,y)" "x ∈ A" "y ∈ B"
      by blast
    show "((f p) < f q) = ((p, q) ∈ (r <*lex*> s))"
    proof
      assume "f p < f q"
      with § assms have "(u, x) ∈ r ∨ u=x ∧ (v, y) ∈ s"
        apply (simp add: f_def)
        by (metis Ord_add Ord_add_mult_iff Ord_mem_iff_lt Ord_mult wf_Ord_ordermap converse_ordermap_mono 
            ordermap_eq_iff ordermap_in_ordertype wf_Ord_ordertype)
      then show "(p,q) ∈ (r <*lex*> s)"
        by (simp add: §)
    next
      assume "(p,q) ∈ (r <*lex*> s)"
      then have "(u, x) ∈ r ∨ u = x ∧ (v, y) ∈ s"
        by (simp add: §)
      then show "f p < f q"
      proof
        assume ux: "(u, x) ∈ r"
        have oo: "⋀x. Ord (ordermap A r x)" "⋀y. Ord (ordermap B s y)" 
          by (simp_all add: r s)
        show "f p < f q"
        proof (clarsimp simp: f_def split: prod.split)
          fix a b a' b'
          assume "p = (a, b)" and "q = (a', b')"
          then have "?β * ordermap A r a + ordermap B s b < ?β * ordermap A r a'"
            using ux assms §
            by (metis Ord_mult wf_Ord_ordermap OrdmemD Pair_inject add_mult_less ordermap_in_ordertype ordermap_mono wf_Ord_ordertype)
          also have "… ≤ ?β * ordermap A r a' + ordermap B s b'"
            by simp
          finally show "?β * ordermap A r a + ordermap B s b < ?β * ordermap A r a' + ordermap B s b'" .
        qed
      next
        assume "u = x ∧ (v, y) ∈ s"
        then show "f p < f q"
          using § assms by (fastforce simp: f_def split: prod.split intro: ordermap_mono_less)
      qed 
    qed
  qed 
qed (use assms small_Times in auto)

end