Theory OrderedGroup_ZF

(*    This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2005, 2006  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

section ‹Ordered groups - introduction›

theory OrderedGroup_ZF imports Group_ZF_1 AbelianGroup_ZF Finite_ZF_1 OrderedLoop_ZF

begin

text‹This theory file defines and shows the basic properties of (partially
  or linearly) ordered groups. 
  We show that in linearly ordered groups finite sets are bounded 
  and provide a sufficient condition for bounded sets to be finite. This 
  allows to show in ‹Int_ZF_IML.thy› that subsets of integers are 
  bounded iff they are finite.
  Some theorems proven here are properties of ordered loops rather that groups.
  However, for now the development is independent from the material in the ‹OrderedLoop_ZF› theory,
  we just import the definitions of ‹NonnegativeSet› and ‹PositiveSet› from there.›

subsection‹Ordered groups›

text‹This section defines ordered groups and various related notions.›

text‹An ordered group is a group equipped with a partial order that is
  "translation invariant", that is if $a\leq b$ then $a\cdot g \leq b\cdot g$
  and $g\cdot a \leq g\cdot b$.›

definition
  "IsAnOrdGroup(G,P,r) ≡ 
  (IsAgroup(G,P) ∧ r⊆G×G ∧ IsPartOrder(G,r) ∧ (∀g∈G. ∀a b. 
  ⟨a,b⟩ ∈ r ⟶ ⟨P`⟨ a,g⟩,P`⟨ b,g⟩ ⟩ ∈ r ∧ ⟨ P`⟨ g,a⟩,P`⟨ g,b⟩ ⟩ ∈ r ) )"


text‹We also define 
  the absolute value as a ZF-function that is the 
  identity on $G^+$ and the group inverse on the rest of the group.›

definition
  "AbsoluteValue(G,P,r) ≡ id(Nonnegative(G,P,r)) ∪ 
  restrict(GroupInv(G,P),G - Nonnegative(G,P,r))"

text‹The odd functions are defined as those having property 
  $f(a^{-1})=(f(a))^{-1}$. This looks a bit strange in the 
  multiplicative notation, I have to admit.
  For linearly ordered groups a function $f$ defined on the set of positive
  elements iniquely defines an odd function of the whole group. This function
  is called an odd extension of $f$›

definition
  "OddExtension(G,P,r,f) ≡ 
  (f ∪ {⟨a, GroupInv(G,P)`(f`(GroupInv(G,P)`(a)))⟩. 
  a ∈ GroupInv(G,P)``(PositiveSet(G,P,r))} ∪ 
  {⟨TheNeutralElement(G,P),TheNeutralElement(G,P)⟩})"

text‹We will use a similar notation for ordered groups as for the generic 
  groups. ‹G+› denotes the set of nonnegative elements 
  (that satisfy $1\leq a$) and ‹G+› is the set of (strictly) positive
  elements. ‹\<sm>A› is the set inverses of elements from $A$. I hope 
  that using additive notation for this notion is not too shocking here. 
  The symbol ‹f°› denotes the odd extension of $f$. For a function
  defined on $G_+$ this is the unique odd function on $G$ that is 
  equal to $f$ on $G_+$.›

locale group3 =

  fixes G and P and r

  assumes ordGroupAssum: "IsAnOrdGroup(G,P,r)"

  fixes unit ("𝟭")
  defines unit_def [simp]: "𝟭 ≡ TheNeutralElement(G,P)"

  fixes groper (infixl "⋅" 70)
  defines groper_def [simp]: "a ⋅ b ≡ P`⟨ a,b⟩"

  fixes inv ("_¯ " [90] 91)
  defines inv_def [simp]: "x¯ ≡ GroupInv(G,P)`(x)"

  fixes lesseq (infix "\<lsq>" 68)
  defines lesseq_def [simp]: "a \<lsq> b ≡ ⟨ a,b⟩ ∈ r"

  fixes sless (infix "\<ls>" 68)
  defines sless_def [simp]: "a \<ls> b ≡ a\<lsq>b ∧ a≠b"

  fixes nonnegative ("G+")
  defines nonnegative_def [simp]: "G+ ≡ Nonnegative(G,P,r)"

  fixes positive ("G+")
  defines positive_def [simp]: "G+ ≡ PositiveSet(G,P,r)"
  
  fixes setinv ("\<sm> _" 72)
  defines setninv_def [simp]: "\<sm>A ≡ GroupInv(G,P)``(A)"

  fixes abs ("¦ _ ¦")
  defines abs_def [simp]: "¦a¦ ≡ AbsoluteValue(G,P,r)`(a)"

  fixes oddext ("_ °")
  defines oddext_def [simp]: "f° ≡ OddExtension(G,P,r,f)"


text‹In ‹group3› context we can use the theorems proven in the 
  ‹group0› context.›

lemma (in group3) OrderedGroup_ZF_1_L1: shows "group0(G,P)"
  using ordGroupAssum IsAnOrdGroup_def group0_def by simp

text‹Ordered group (carrier) is not empty. This is a property of
  monoids, but it is good to have it handy in the ‹group3› context.›

lemma (in group3) OrderedGroup_ZF_1_L1A: shows "G≠0"
  using OrderedGroup_ZF_1_L1 group0.group0_2_L1 monoid0.group0_1_L3A
  by blast
  
text‹The next lemma is just to see the definition of the nonnegative set
  in our notation.›

lemma (in group3) OrderedGroup_ZF_1_L2: 
  shows "g∈G+ ⟷ 𝟭\<lsq>g"
  using ordGroupAssum IsAnOrdGroup_def Nonnegative_def 
  by auto

text‹The next lemma is just to see the definition of the positive set
  in our notation.›

lemma (in group3) OrderedGroup_ZF_1_L2A: 
  shows "g∈G+ ⟷ (𝟭\<lsq>g ∧ g≠𝟭)"
  using ordGroupAssum IsAnOrdGroup_def PositiveSet_def 
  by auto

text‹For total order if $g$ is not in $G^{+}$, then it has to be 
  less or equal the unit.›

lemma (in group3) OrderedGroup_ZF_1_L2B: 
  assumes A1: "r {is total on} G" and A2: "a∈G-G+"
  shows "a\<lsq>𝟭"
proof -
  from A2 have "a∈G"   "𝟭 ∈ G"  "¬(𝟭\<lsq>a)" 
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2 OrderedGroup_ZF_1_L2 
    by auto
  with A1 show ?thesis using IsTotal_def by auto
qed

text‹The group order is reflexive.›

lemma (in group3) OrderedGroup_ZF_1_L3: assumes "g∈G"
  shows "g\<lsq>g"
  using ordGroupAssum assms IsAnOrdGroup_def IsPartOrder_def refl_def
  by simp

text‹$1$ is nonnegative.›

lemma (in group3) OrderedGroup_ZF_1_L3A: shows "𝟭∈G+"
  using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_1_L3
    OrderedGroup_ZF_1_L1 group0.group0_2_L2 by simp
  
text‹In this context $a \leq b$ implies that both $a$ and $b$ belong 
  to $G$.›

lemma (in group3) OrderedGroup_ZF_1_L4: 
  assumes "a\<lsq>b" shows "a∈G" "b∈G"
  using ordGroupAssum assms IsAnOrdGroup_def by auto

text‹Similarly in this context $a \le b$ implies that both $a$ and $b$ belong 
  to $G$.›

lemma (in group3) less_are_members: 
  assumes "a\<ls>b" shows "a∈G" "b∈G"
  using ordGroupAssum assms IsAnOrdGroup_def by auto

text‹It is good to have transitivity handy.›

lemma (in group3) Group_order_transitive:
  assumes A1: "a\<lsq>b"  "b\<lsq>c" shows "a\<lsq>c"
proof -
  from ordGroupAssum have "trans(r)"
    using IsAnOrdGroup_def IsPartOrder_def
    by simp
  moreover from A1 have "⟨ a,b⟩ ∈ r ∧ ⟨ b,c⟩ ∈ r" by simp
  ultimately have "⟨ a,c⟩ ∈ r" by (rule Fol1_L3)
  thus ?thesis by simp
qed

text‹The order in an ordered group is antisymmetric.›

lemma (in group3) group_order_antisym:
  assumes A1: "a\<lsq>b"  "b\<lsq>a" shows "a=b"
proof -
  from ordGroupAssum A1 have 
    "antisym(r)"  "⟨ a,b⟩ ∈ r"  "⟨ b,a⟩ ∈ r"
    using IsAnOrdGroup_def IsPartOrder_def by auto
  then show "a=b" by (rule Fol1_L4) 
qed

text‹Transitivity for the strict order: if $a < b$ and $b\leq c$, then $a < c$.›

lemma (in group3) OrderedGroup_ZF_1_L4A:
  assumes A1: "a\<ls>b"  and A2: "b\<lsq>c"
  shows "a\<ls>c"
proof -
  from A1 A2 have "a\<lsq>b"  "b\<lsq>c" by auto
  then have "a\<lsq>c" by (rule Group_order_transitive)
  moreover from A1 A2 have "a≠c" using group_order_antisym by auto
  ultimately show "a\<ls>c" by simp
qed

text‹Another version of transitivity for the strict order: 
  if $a\leq b$ and $b < c$, then $a < c$.›

lemma (in group3) group_strict_ord_transit:
  assumes A1: "a\<lsq>b" and A2: "b\<ls>c"
  shows "a\<ls>c"
proof -
  from A1 A2 have "a\<lsq>b"  "b\<lsq>c" by auto
  then have  "a\<lsq>c" by (rule Group_order_transitive)
  moreover from A1 A2 have "a≠c" using group_order_antisym by auto
  ultimately show "a\<ls>c" by simp
qed

text‹The order is translation invariant. ›

lemma (in group3) ord_transl_inv: assumes "a\<lsq>b" "c∈G"
  shows "a⋅c \<lsq> b⋅c" and "c⋅a \<lsq> c⋅b"
  using ordGroupAssum assms unfolding IsAnOrdGroup_def by auto

text‹Strict order is preserved by translations.›

lemma (in group3) group_strict_ord_transl_inv: 
  assumes "a\<ls>b" and "c∈G"
  shows "a⋅c \<ls> b⋅c" and "c⋅a \<ls> c⋅b"
  using assms ord_transl_inv OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 group0.group0_2_L19 
  by auto

text‹If the group order is total, then the group is ordered linearly.›

lemma (in group3) group_ord_total_is_lin:
  assumes "r {is total on} G"
  shows "IsLinOrder(G,r)"
  using assms ordGroupAssum IsAnOrdGroup_def Order_ZF_1_L3
  by simp

text‹For linearly ordered groups elements in the nonnegative set are
  greater than those in the complement.›

lemma (in group3) OrderedGroup_ZF_1_L4B:
  assumes "r {is total on} G" 
  and "a∈G+" and "b ∈ G-G+"
  shows "b\<lsq>a"
proof -
  from assms have "b\<lsq>𝟭" "𝟭\<lsq>a"
    using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_1_L2B by auto
  then show ?thesis by (rule Group_order_transitive)
qed

text‹If $a\leq 1$ and $a\neq 1$, then $a \in G\setminus G^{+}$.›

lemma (in group3) OrderedGroup_ZF_1_L4C:
  assumes A1: "a\<lsq>𝟭" and A2: "a≠𝟭"
  shows "a ∈ G-G+"
proof - 
  { assume "a ∉ G-G+" 
    with ordGroupAssum A1 A2 have False 
      using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L2
	OrderedGroup_ZF_1_L4 IsAnOrdGroup_def IsPartOrder_def antisym_def
      by auto
  } thus ?thesis by auto
qed

text‹An element smaller than an element in $G\setminus G^+$ is in 
  $G\setminus G^+$.›

lemma (in group3) OrderedGroup_ZF_1_L4D:
  assumes A1: "a∈G-G+" and A2: "b\<lsq>a"
  shows "b∈G-G+"
proof - 
  { assume "b ∉ G - G+"
    with A2 have "𝟭\<lsq>b" "b\<lsq>a"
      using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L2 by auto
    then have "𝟭\<lsq>a" by (rule Group_order_transitive)
    with A1 have False using OrderedGroup_ZF_1_L2 by simp
  } thus ?thesis by auto
qed

text‹The nonnegative set is contained in the group.›

lemma (in group3) OrderedGroup_ZF_1_L4E: shows "G+ ⊆ G"
  using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_1_L4 by auto

text‹The positive set is contained in the nonnegative set, hence in the group.›

lemma (in group3) pos_set_in_gr: shows "G+ ⊆ G+" and "G+ ⊆ G"
  using OrderedGroup_ZF_1_L2A OrderedGroup_ZF_1_L2 OrderedGroup_ZF_1_L4E
  by auto  

text‹Taking the inverse on both sides reverses the inequality.›

lemma (in group3) OrderedGroup_ZF_1_L5:
  assumes A1: "a\<lsq>b" shows "b¯\<lsq>a¯"
proof -
  from A1 have T1: "a∈G" "b∈G" "a¯∈G" "b¯∈G" 
    using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 
      group0.inverse_in_group by auto
  with A1 ordGroupAssum have "a⋅a¯\<lsq>b⋅a¯" using IsAnOrdGroup_def
    by simp
  with T1 ordGroupAssum have "b¯⋅𝟭\<lsq>b¯⋅(b⋅a¯)"
    using OrderedGroup_ZF_1_L1 group0.group0_2_L6 IsAnOrdGroup_def
    by simp
  with T1 show ?thesis using
    OrderedGroup_ZF_1_L1 group0.group0_2_L2 group0.group_oper_assoc
    group0.group0_2_L6 by simp
qed

text‹If an element is smaller that the unit, then its inverse is greater.›

lemma (in group3) OrderedGroup_ZF_1_L5A: 
  assumes A1: "a\<lsq>𝟭" shows "𝟭\<lsq>a¯"
proof -
  from A1 have "𝟭¯\<lsq>a¯" using OrderedGroup_ZF_1_L5
    by simp
  then show ?thesis using OrderedGroup_ZF_1_L1 group0.group_inv_of_one 
    by simp
qed

text‹If an the inverse of an element is greater that the unit, 
  then the element is smaller.›

lemma (in group3) OrderedGroup_ZF_1_L5AA: 
  assumes A1: "a∈G" and A2: "𝟭\<lsq>a¯"  
  shows "a\<lsq>𝟭"
proof -
  from A2 have "(a¯)¯\<lsq>𝟭¯" using OrderedGroup_ZF_1_L5
    by simp
  with A1 show "a\<lsq>𝟭"
    using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv group0.group_inv_of_one
    by simp
qed

text‹If an element is nonnegative, then the inverse is 
  not greater that the unit.
  Also shows that nonnegative elements cannot be negative›

lemma (in group3) OrderedGroup_ZF_1_L5AB:
  assumes A1: "𝟭\<lsq>a" shows "a¯\<lsq>𝟭" and "¬(a\<lsq>𝟭 ∧ a≠𝟭)"
proof -
  from A1 have "a¯\<lsq>𝟭¯"
    using OrderedGroup_ZF_1_L5 by simp
  then show "a¯\<lsq>𝟭" using OrderedGroup_ZF_1_L1 group0.group_inv_of_one
    by simp
  { assume "a\<lsq>𝟭" and "a≠𝟭"
    with A1 have False using group_order_antisym
      by blast
  } then show "¬(a\<lsq>𝟭 ∧ a≠𝟭)" by auto
qed

text‹If two elements are greater or equal than the unit, then the inverse
  of one is not greater than the other.›

lemma (in group3) OrderedGroup_ZF_1_L5AC:
  assumes A1: "𝟭\<lsq>a"  "𝟭\<lsq>b"
  shows "a¯ \<lsq> b"
proof -
  from A1 have "a¯\<lsq>𝟭"  "𝟭\<lsq>b"
    using OrderedGroup_ZF_1_L5AB by auto
  then show "a¯ \<lsq> b" by (rule Group_order_transitive)
qed

subsection‹Inequalities›

text‹This section developes some simple tools to deal with inequalities.›


text‹Taking negative on both sides reverses the inequality, case with
  an inverse on one side.›

lemma (in group3) OrderedGroup_ZF_1_L5AD:
  assumes A1: "b ∈ G" and A2: "a\<lsq>b¯"
  shows "b \<lsq> a¯"
proof -
  from A2 have "(b¯)¯ \<lsq> a¯"
    using OrderedGroup_ZF_1_L5 by simp
  with A1 show "b \<lsq> a¯"
    using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
    by simp
qed

text‹We can cancel the same element on both sides of an inequality.›

lemma (in group3) OrderedGroup_ZF_1_L5AE:
  assumes A1: "a∈G"  "b∈G"  "c∈G" and A2: "a⋅b \<lsq> a⋅c"
  shows "b\<lsq>c"
proof -
  from ordGroupAssum A1 A2 have "a¯⋅(a⋅b) \<lsq> a¯⋅(a⋅c)"
    using OrderedGroup_ZF_1_L1 group0.inverse_in_group IsAnOrdGroup_def 
    by simp
  with A1 show "b\<lsq>c" 
    using OrderedGroup_ZF_1_L1 group0.inv_cancel_two
    by simp
qed

text‹We can cancel the same element on both sides of an inequality, right side.›

lemma (in group3) ineq_cancel_right:
  assumes "a∈G"  "b∈G"  "c∈G" and "a⋅b \<lsq> c⋅b"
  shows "a\<lsq>c"
proof -
  from assms(2,4) have "(a⋅b)⋅b¯ \<lsq> (c⋅b)⋅b¯"
    using OrderedGroup_ZF_1_L1 group0.inverse_in_group ord_transl_inv(1) by simp
  with assms(1,2,3) show "a\<lsq>c" using OrderedGroup_ZF_1_L1 group0.inv_cancel_two(2) 
    by auto
qed

text‹We can cancel the same element on both sides of an inequality,
  a version with an inverse on both sides.›

lemma (in group3) OrderedGroup_ZF_1_L5AF:
  assumes A1: "a∈G"  "b∈G"  "c∈G" and A2: "a⋅b¯ \<lsq> a⋅c¯"
  shows "c\<lsq>b"
proof -
  from A1 A2 have "(c¯)¯ \<lsq> (b¯)¯"
     using OrderedGroup_ZF_1_L1 group0.inverse_in_group 
      OrderedGroup_ZF_1_L5AE OrderedGroup_ZF_1_L5 by simp
  with A1 show "c\<lsq>b" 
    using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv by simp
qed

text‹Taking negative on both sides reverses the inequality, another case with
  an inverse on one side.›

lemma (in group3) OrderedGroup_ZF_1_L5AG:
  assumes A1: "a ∈ G" and A2: "a¯\<lsq>b"
  shows "b¯ \<lsq> a"
proof -
  from A2 have "b¯ \<lsq> (a¯)¯"
    using OrderedGroup_ZF_1_L5 by simp
  with A1 show "b¯ \<lsq> a"
    using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
    by simp
qed
  
text‹We can multiply the sides of two inequalities.›

lemma (in group3) OrderedGroup_ZF_1_L5B:
  assumes A1: "a\<lsq>b" and A2: "c\<lsq>d"
  shows "a⋅c \<lsq> b⋅d"
proof -
  from A1 A2 have "c∈G" "b∈G" using OrderedGroup_ZF_1_L4 by auto
  with A1 A2 ordGroupAssum have "a⋅c\<lsq> b⋅c" "b⋅c\<lsq>b⋅d"
    using IsAnOrdGroup_def by auto
  then show "a⋅c \<lsq> b⋅d" by (rule Group_order_transitive)
qed

text‹We can replace first of the factors on one side of an inequality 
  with a greater one.›

lemma (in group3) OrderedGroup_ZF_1_L5C: 
  assumes A1: "c∈G" and A2: "a\<lsq>b⋅c" and A3: "b\<lsq>b1" 
  shows "a\<lsq>b1⋅c"
proof -
  from A1 A3 have "b⋅c \<lsq> b1⋅c"
    using OrderedGroup_ZF_1_L3 OrderedGroup_ZF_1_L5B by simp
  with A2 show "a\<lsq>b1⋅c" by (rule Group_order_transitive)
qed

text‹We can replace second of the factors on one side of an inequality 
  with a greater one.›

lemma (in group3) OrderedGroup_ZF_1_L5D: 
  assumes A1: "b∈G" and A2: "a \<lsq> b⋅c" and A3: "c\<lsq>b1" 
  shows "a \<lsq> b⋅b1"
proof -
  from A1 A3 have "b⋅c \<lsq> b⋅b1"
    using OrderedGroup_ZF_1_L3 OrderedGroup_ZF_1_L5B by auto
  with A2 show "a\<lsq>b⋅b1" by (rule Group_order_transitive)
qed

text‹We can replace factors on one side of an inequality 
  with greater ones.›

lemma (in group3) OrderedGroup_ZF_1_L5E: 
  assumes A1: "a \<lsq> b⋅c" and A2: "b\<lsq>b1"  "c\<lsq>c1"  
  shows "a \<lsq> b1⋅c1"
proof -
  from A2 have "b⋅c \<lsq> b1⋅c1" using OrderedGroup_ZF_1_L5B 
    by simp
  with A1 show "a\<lsq>b1⋅c1" by (rule Group_order_transitive)
qed

text‹We don't decrease an element of the group by multiplying by one that is
  nonnegative.›

lemma (in group3) OrderedGroup_ZF_1_L5F:
  assumes A1: "𝟭\<lsq>a" and A2: "b∈G"
  shows "b\<lsq>a⋅b"  "b\<lsq>b⋅a" 
proof -
  from ordGroupAssum A1 A2 have  
    "𝟭⋅b\<lsq>a⋅b"  "b⋅𝟭\<lsq>b⋅a"
    using IsAnOrdGroup_def by auto
  with A2 show "b\<lsq>a⋅b"  "b\<lsq>b⋅a"
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by auto
qed

text‹We can multiply the right hand side of an inequality by a nonnegative
  element.›

lemma (in group3) OrderedGroup_ZF_1_L5G: assumes A1: "a\<lsq>b"
  and A2: "𝟭\<lsq>c" shows "a\<lsq>b⋅c"  "a\<lsq>c⋅b" 
proof -
  from A1 A2 have I: "b\<lsq>b⋅c"  and II: "b\<lsq>c⋅b"
    using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L5F by auto
  from A1 I show "a\<lsq>b⋅c" by (rule Group_order_transitive)
  from A1 II show "a\<lsq>c⋅b" by (rule Group_order_transitive)
qed

text‹We can put two elements on the other side of inequality, 
  changing their sign.›

lemma (in group3) OrderedGroup_ZF_1_L5H: 
  assumes A1: "a∈G"  "b∈G" and A2: "a⋅b¯ \<lsq> c"
  shows 
  "a \<lsq> c⋅b"
  "c¯⋅a \<lsq> b"
proof -
  from A2 have T: "c∈G"  "c¯ ∈ G"
    using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 
      group0.inverse_in_group by auto
  from ordGroupAssum A1 A2 have "a⋅b¯⋅b \<lsq> c⋅b"
    using IsAnOrdGroup_def by simp
  with A1 show "a \<lsq> c⋅b" 
    using OrderedGroup_ZF_1_L1 group0.inv_cancel_two
    by simp
  with ordGroupAssum A2 T have "c¯⋅a \<lsq> c¯⋅(c⋅b)"
    using IsAnOrdGroup_def by simp
  with A1 T show "c¯⋅a \<lsq> b"  
    using OrderedGroup_ZF_1_L1 group0.inv_cancel_two
    by simp
qed

text‹We can multiply the sides of one inequality by inverse of another.›

lemma (in group3) OrderedGroup_ZF_1_L5I: 
  assumes "a\<lsq>b" and "c\<lsq>d"
  shows "a⋅d¯ \<lsq> b⋅c¯"
  using assms OrderedGroup_ZF_1_L5 OrderedGroup_ZF_1_L5B
  by simp

text‹We can put an element on the other side of an inequality
  changing its sign, version with the inverse.›

lemma (in group3) OrderedGroup_ZF_1_L5J:
  assumes A1: "a∈G"  "b∈G" and A2: "c \<lsq> a⋅b¯"
  shows "c⋅b \<lsq> a"
proof -
  from ordGroupAssum A1 A2 have "c⋅b \<lsq> a⋅b¯⋅b"
    using IsAnOrdGroup_def by simp
  with A1 show "c⋅b \<lsq> a" 
    using OrderedGroup_ZF_1_L1 group0.inv_cancel_two
    by simp
qed

text‹We can put an element on the other side of an inequality
  changing its sign, version with the inverse.›

lemma (in group3) OrderedGroup_ZF_1_L5JA:
  assumes A1: "a∈G"  "b∈G" and A2: "c \<lsq> a¯⋅b"
  shows "a⋅c\<lsq> b"
proof -
  from ordGroupAssum A1 A2 have "a⋅c \<lsq> a⋅(a¯⋅b)"
    using IsAnOrdGroup_def by simp
  with A1 show "a⋅c\<lsq> b" 
    using OrderedGroup_ZF_1_L1 group0.inv_cancel_two
    by simp
qed
    

text‹A special case of ‹OrderedGroup_ZF_1_L5J› where $c=1$.›

corollary (in group3) OrderedGroup_ZF_1_L5K: 
  assumes A1: "a∈G"  "b∈G" and A2: "𝟭 \<lsq> a⋅b¯"
  shows "b \<lsq> a"
proof -
  from A1 A2 have "𝟭⋅b \<lsq> a"
    using OrderedGroup_ZF_1_L5J by simp
  with A1 show "b \<lsq> a"
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by simp
qed

text‹A special case of ‹OrderedGroup_ZF_1_L5JA› where $c=1$.›

corollary (in group3) OrderedGroup_ZF_1_L5KA: 
  assumes A1: "a∈G"  "b∈G" and A2: "𝟭 \<lsq> a¯⋅b"
  shows "a \<lsq> b"
proof -
  from A1 A2 have "a⋅𝟭 \<lsq> b"
    using OrderedGroup_ZF_1_L5JA by simp
  with A1 show "a \<lsq> b"
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by simp
qed

text‹If the order is total, the elements that do not belong
  to the positive set are negative. We also show here that the group inverse
  of an element that does not belong to the nonnegative set does belong to the
  nonnegative set.›

lemma (in group3) OrderedGroup_ZF_1_L6: 
  assumes A1: "r {is total on} G" and A2: "a∈G-G+"
  shows "a\<lsq>𝟭"  "a¯ ∈ G+"  "restrict(GroupInv(G,P),G-G+)`(a) ∈ G+" 
proof - 
  from A2 have T1: "a∈G" "a∉G+" "𝟭∈G" 
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2 by auto
  with A1 show "a\<lsq>𝟭" using OrderedGroup_ZF_1_L2 IsTotal_def
    by auto
  then show "a¯ ∈ G+" using OrderedGroup_ZF_1_L5A OrderedGroup_ZF_1_L2
    by simp
  with A2 show "restrict(GroupInv(G,P),G-G+)`(a) ∈ G+"
    using restrict by simp
qed

text‹If a property is invariant with respect to taking the inverse
  and it is true on the nonnegative set, than it is true on the whole
  group.›

lemma (in group3) OrderedGroup_ZF_1_L7:
  assumes A1: "r {is total on} G"
  and A2: "∀a∈G+.∀b∈G+. Q(a,b)"
  and A3: "∀a∈G.∀b∈G. Q(a,b)⟶Q(a¯,b)"
  and A4: "∀a∈G.∀b∈G. Q(a,b)⟶Q(a,b¯)"
  and A5: "a∈G" "b∈G"
  shows "Q(a,b)"
proof -
  { assume A6: "a∈G+" have "Q(a,b)"
    proof -
      { assume "b∈G+" 
	with A6 A2 have "Q(a,b)" by simp }
      moreover
      { assume "b∉G+"
	with A1 A2 A4 A5 A6 have "Q(a,(b¯)¯)"  
	  using OrderedGroup_ZF_1_L6 OrderedGroup_ZF_1_L1 group0.inverse_in_group
	  by simp
	with A5 have "Q(a,b)" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
	  by simp }
      ultimately show "Q(a,b)" by auto
    qed }
  moreover
  { assume "a∉G+"
    with A1 A5 have T1: "a¯ ∈ G+" using OrderedGroup_ZF_1_L6 by simp
    have "Q(a,b)"
    proof -
      { assume "b∈G+"
	with A2 A3 A5 T1 have "Q((a¯)¯,b)" 
	  using OrderedGroup_ZF_1_L1 group0.inverse_in_group by simp
	with A5 have "Q(a,b)" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
	  by simp }
      moreover
      { assume "b∉G+"
	with A1 A2 A3 A4 A5 T1 have "Q((a¯)¯,(b¯)¯)"
	  using OrderedGroup_ZF_1_L6 OrderedGroup_ZF_1_L1 group0.inverse_in_group
	  by simp
	with A5 have "Q(a,b)" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
	  by simp }
      ultimately show "Q(a,b)" by auto
    qed }
  ultimately show "Q(a,b)" by auto
qed

text‹A lemma about splitting the ordered group "plane" into 6 subsets. Useful
  for proofs by cases.›

lemma (in group3) OrdGroup_6cases: assumes A1: "r {is total on} G" 
  and A2:  "a∈G"  "b∈G"
  shows 
  "𝟭\<lsq>a ∧ 𝟭\<lsq>b  ∨  a\<lsq>𝟭 ∧ b\<lsq>𝟭  ∨  
  a\<lsq>𝟭 ∧ 𝟭\<lsq>b ∧ 𝟭 \<lsq> a⋅b  ∨ a\<lsq>𝟭 ∧ 𝟭\<lsq>b ∧ a⋅b \<lsq> 𝟭  ∨  
  𝟭\<lsq>a ∧ b\<lsq>𝟭 ∧ 𝟭 \<lsq> a⋅b  ∨  𝟭\<lsq>a ∧ b\<lsq>𝟭 ∧ a⋅b \<lsq> 𝟭"
proof -
  from A1 A2 have 
    "𝟭\<lsq>a ∨ a\<lsq>𝟭"   
    "𝟭\<lsq>b ∨ b\<lsq>𝟭"
    "𝟭 \<lsq> a⋅b ∨ a⋅b \<lsq> 𝟭"
    using OrderedGroup_ZF_1_L1 group0.group_op_closed group0.group0_2_L2
      IsTotal_def by auto
  then show ?thesis by auto
qed

text‹The next lemma shows what happens when one element of a totally 
  ordered group is not greater or equal than another.›

lemma (in group3) OrderedGroup_ZF_1_L8:
  assumes A1: "r {is total on} G"
  and A2: "a∈G"  "b∈G"
  and A3: "¬(a\<lsq>b)"
  shows "b \<lsq> a"  "a¯ \<lsq> b¯"  "a≠b"  "b\<ls>a"
 
proof -
  from A1 A2 A3 show I: "b \<lsq> a" using IsTotal_def
    by auto
  then show "a¯ \<lsq> b¯" using OrderedGroup_ZF_1_L5 by simp
  from A2 have "a \<lsq> a" using OrderedGroup_ZF_1_L3 by simp
  with I A3 show "a≠b"  "b \<ls> a" by auto
qed

text‹If one element is greater or equal and not equal to another,
  then it is not smaller or equal.›

lemma (in group3) OrderedGroup_ZF_1_L8AA: 
  assumes A1: "a\<lsq>b" and A2: "a≠b"
  shows "¬(b\<lsq>a)"
proof -
  { note A1
    moreover assume "b\<lsq>a"
    ultimately have "a=b" by (rule group_order_antisym)
    with A2 have False by simp
  } thus "¬(b\<lsq>a)" by auto
qed

text‹A special case of ‹OrderedGroup_ZF_1_L8› when one of 
  the elements is the unit.›

corollary (in group3) OrderedGroup_ZF_1_L8A:
  assumes A1: "r {is total on} G"
  and A2: "a∈G" and A3: "¬(𝟭\<lsq>a)"
  shows "𝟭 \<lsq> a¯"  "𝟭≠a"  "a\<lsq>𝟭"
proof -
  from A1 A2 A3 have I:
    "r {is total on} G"
    "𝟭∈G"  "a∈G"
     "¬(𝟭\<lsq>a)"
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by auto
  then have "𝟭¯ \<lsq> a¯"
    by (rule OrderedGroup_ZF_1_L8)
  then show "𝟭 \<lsq> a¯"
    using OrderedGroup_ZF_1_L1 group0.group_inv_of_one by simp
  from I show "𝟭≠a" by (rule OrderedGroup_ZF_1_L8)
  from A1 I show "a\<lsq>𝟭" using IsTotal_def
    by auto
qed

text‹A negative element can not be nonnegative.›

lemma (in group3) OrderedGroup_ZF_1_L8B:
  assumes A1: "a\<lsq>𝟭"  and A2: "a≠𝟭" shows "¬(𝟭\<lsq>a)"
proof -
  { assume  "𝟭\<lsq>a" 
    with A1 have "a=𝟭" using group_order_antisym
      by auto
    with A2 have False by simp
  } thus ?thesis by auto
qed

text‹An element is greater or equal than another iff the difference is 
  nonpositive.›

lemma (in group3) OrderedGroup_ZF_1_L9:
  assumes A1: "a∈G"  "b∈G"
  shows "a\<lsq>b ⟷ a⋅b¯ \<lsq> 𝟭"
proof
  assume "a \<lsq> b"
  with ordGroupAssum A1 have "a⋅b¯ \<lsq> b⋅b¯"
    using OrderedGroup_ZF_1_L1 group0.inverse_in_group
    IsAnOrdGroup_def by simp
  with A1 show "a⋅b¯ \<lsq> 𝟭" 
    using OrderedGroup_ZF_1_L1 group0.group0_2_L6
    by simp
next assume A2: "a⋅b¯ \<lsq> 𝟭"
  with ordGroupAssum A1 have "a⋅b¯⋅b \<lsq> 𝟭⋅b"
    using IsAnOrdGroup_def by simp
  with A1 show "a \<lsq> b"
    using OrderedGroup_ZF_1_L1 
      group0.inv_cancel_two group0.group0_2_L2 
    by simp
qed

text‹We can move an element to the other side of an inequality.›

lemma (in group3) OrderedGroup_ZF_1_L9A:
  assumes A1: "a∈G"  "b∈G"  "c∈G"
  shows "a⋅b \<lsq> c  ⟷ a \<lsq> c⋅b¯"
proof
  assume "a⋅b \<lsq> c"
  with ordGroupAssum A1 have "a⋅b⋅b¯ \<lsq> c⋅b¯"
    using OrderedGroup_ZF_1_L1 group0.inverse_in_group IsAnOrdGroup_def
    by simp
  with A1 show "a \<lsq> c⋅b¯"
    using OrderedGroup_ZF_1_L1 group0.inv_cancel_two by simp
next assume "a \<lsq> c⋅b¯"
  with ordGroupAssum A1 have "a⋅b \<lsq> c⋅b¯⋅b"
    using OrderedGroup_ZF_1_L1 group0.inverse_in_group IsAnOrdGroup_def
    by simp
  with A1 show "a⋅b \<lsq> c"
     using OrderedGroup_ZF_1_L1 group0.inv_cancel_two by simp
qed

text‹A one side version of the previous lemma with weaker assuptions.›

lemma (in group3) OrderedGroup_ZF_1_L9B:
  assumes A1: "a∈G"  "b∈G" and A2: "a⋅b¯ \<lsq> c"
  shows "a \<lsq> c⋅b"
proof - 
  from A1 A2 have "a∈G"  "b¯∈G"  "c∈G"
    using OrderedGroup_ZF_1_L1 group0.inverse_in_group 
      OrderedGroup_ZF_1_L4 by auto
  with A1 A2 show "a \<lsq> c⋅b"
    using OrderedGroup_ZF_1_L9A OrderedGroup_ZF_1_L1 
      group0.group_inv_of_inv by simp
qed

text‹We can put en element on the other side of inequality, 
  changing its sign.›

lemma (in group3) OrderedGroup_ZF_1_L9C:
  assumes A1: "a∈G"  "b∈G" and A2: "c\<lsq>a⋅b"
  shows 
  "c⋅b¯ \<lsq> a"
  "a¯⋅c \<lsq> b"
proof -
  from ordGroupAssum A1 A2 have
    "c⋅b¯ \<lsq> a⋅b⋅b¯"
    "a¯⋅c \<lsq> a¯⋅(a⋅b)"
    using OrderedGroup_ZF_1_L1 group0.inverse_in_group IsAnOrdGroup_def
    by auto
  with A1 show  
    "c⋅b¯ \<lsq> a"
    "a¯⋅c \<lsq> b"
    using OrderedGroup_ZF_1_L1 group0.inv_cancel_two
    by auto
qed

text‹If an element is greater or equal than another then the difference is 
  nonnegative.›

lemma (in group3) OrderedGroup_ZF_1_L9D: assumes A1: "a\<lsq>b"
  shows "𝟭 \<lsq> b⋅a¯"
proof -
  from A1 have T: "a∈G"  "b∈G"   "a¯ ∈ G" 
    using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 
      group0.inverse_in_group by auto
  with ordGroupAssum A1 have "a⋅a¯ \<lsq> b⋅a¯"
    using IsAnOrdGroup_def by simp
  with T show "𝟭 \<lsq> b⋅a¯" 
    using OrderedGroup_ZF_1_L1 group0.group0_2_L6
    by simp
qed

text‹If an element is greater than another then the difference is 
  positive.›

lemma (in group3) OrderedGroup_ZF_1_L9E: 
  assumes A1: "a\<lsq>b"  "a≠b"
  shows "𝟭 \<lsq> b⋅a¯"  "𝟭 ≠ b⋅a¯"  "b⋅a¯ ∈ G+"
proof -
  from A1 have T: "a∈G"  "b∈G" using OrderedGroup_ZF_1_L4
    by auto
  from A1 show I: "𝟭 \<lsq> b⋅a¯" using OrderedGroup_ZF_1_L9D
    by simp
  { assume "b⋅a¯ = 𝟭" 
    with T have "a=b"
      using OrderedGroup_ZF_1_L1 group0.group0_2_L11A
      by auto
    with A1 have False by simp 
  } then show "𝟭 ≠ b⋅a¯" by auto
  then have "b⋅a¯ ≠ 𝟭" by auto
  with I show "b⋅a¯ ∈ G+" using OrderedGroup_ZF_1_L2A
    by simp
qed

text‹If the difference is nonnegative, then $a\leq b$.›

lemma (in group3) OrderedGroup_ZF_1_L9F: 
  assumes A1: "a∈G"  "b∈G" and A2: "𝟭 \<lsq> b⋅a¯"
  shows "a\<lsq>b"
proof -
  from A1 A2 have "𝟭⋅a \<lsq> b"
    using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L9A
    by simp
  with A1 show "a\<lsq>b" 
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by simp
qed


text‹If we increase the middle term in a product, the whole product 
  increases.›

lemma (in group3) OrderedGroup_ZF_1_L10: 
  assumes "a∈G"  "b∈G" and "c\<lsq>d"
  shows "a⋅c⋅b \<lsq> a⋅d⋅b"
  using ordGroupAssum assms IsAnOrdGroup_def by simp

text‹A product of (strictly) positive elements is not the unit.›

lemma (in group3) OrderedGroup_ZF_1_L11: 
  assumes A1: "𝟭\<lsq>a"  "𝟭\<lsq>b"
  and A2: "𝟭 ≠ a"  "𝟭 ≠ b"
  shows "𝟭 ≠ a⋅b"
proof -
  from A1 have T1: "a∈G"  "b∈G"
    using OrderedGroup_ZF_1_L4 by auto
  { assume "𝟭 = a⋅b"
    with A1 T1 have "a\<lsq>𝟭"  "𝟭\<lsq>a"
      using OrderedGroup_ZF_1_L1 group0.group0_2_L9 OrderedGroup_ZF_1_L5AA 
      by auto
    then have "a = 𝟭" by (rule group_order_antisym)
    with A2 have False by simp
  } then show "𝟭 ≠ a⋅b" by auto
qed

text‹A product of nonnegative elements is nonnegative.›

lemma (in group3) OrderedGroup_ZF_1_L12:
  assumes A1: "𝟭 \<lsq> a"  "𝟭 \<lsq> b"
  shows "𝟭 \<lsq> a⋅b"
proof -
  from A1 have "𝟭⋅𝟭 \<lsq> a⋅b"
    using  OrderedGroup_ZF_1_L5B by simp
  then show "𝟭 \<lsq> a⋅b" 
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2 
    by simp
qed

text‹If $a$ is not greater than $b$, then $1$ is not greater than
  $b\cdot a^{-1}$.›

lemma (in group3) OrderedGroup_ZF_1_L12A:
  assumes A1: "a\<lsq>b" shows "𝟭 \<lsq> b⋅a¯"
proof -
  from A1 have T: "𝟭 ∈ G"  "a∈G"  "b∈G" 
    using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by auto
  with A1 have "𝟭⋅a \<lsq> b" 
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by simp
  with T show "𝟭 \<lsq> b⋅a¯" using OrderedGroup_ZF_1_L9A
    by simp
qed
  
text‹We can move an element to the other side of a strict inequality.›

lemma (in group3) OrderedGroup_ZF_1_L12B:  
  assumes A1: "a∈G"  "b∈G" and  A2: "a⋅b¯ \<ls> c"
  shows "a \<ls> c⋅b"
proof -
  from A1 A2 have "a⋅b¯⋅b \<ls> c⋅b"
    using group_strict_ord_transl_inv by auto
  moreover from A1 have "a⋅b¯⋅b = a"
    using OrderedGroup_ZF_1_L1 group0.inv_cancel_two
    by simp
  ultimately show "a \<ls> c⋅b"
    by auto
qed

(*lemma (in group3) OrderedGroup_ZF_1_L12B:  
  assumes A1: "a∈G"  "b∈G" and  A2: "a⋅b¯ \<lsq> c"  "a⋅b¯ ≠ c"
  shows "a \<lsq> c⋅b"  "a ≠ c⋅b"
proof -
  from A1 A2 have "a⋅b¯⋅b \<lsq> c⋅b"  "a⋅b¯⋅b ≠ c⋅b"
    using group_strict_ord_transl_inv by auto
  moreover from A1 have "a⋅b¯⋅b = a"
    using OrderedGroup_ZF_1_L1 group0.inv_cancel_two
    by simp
  ultimately show "a \<lsq> c⋅b"  "a ≠ c⋅b"
    by auto
qed;*)

text‹We can multiply the sides of two inequalities,
  first of them strict and we get a strict inequality.›

lemma (in group3) OrderedGroup_ZF_1_L12C:
  assumes A1: "a\<ls>b" and A2: "c\<lsq>d"
  shows "a⋅c \<ls> b⋅d"
proof -
  from A1 A2 have T: "a∈G"  "b∈G"  "c∈G"  "d∈G"
    using OrderedGroup_ZF_1_L4 by auto
  with ordGroupAssum A2 have "a⋅c \<lsq> a⋅d"
    using IsAnOrdGroup_def by simp
  moreover from A1 T have "a⋅d \<ls> b⋅d"
    using group_strict_ord_transl_inv by simp
  ultimately show "a⋅c \<ls> b⋅d"
    by (rule group_strict_ord_transit)
qed
  
text‹We can multiply the sides of two inequalities,
  second of them strict and we get a strict inequality.›

lemma (in group3) OrderedGroup_ZF_1_L12D:
  assumes A1: "a\<lsq>b" and A2: "c\<ls>d"
  shows "a⋅c \<ls> b⋅d"
proof -
  from A1 A2 have T: "a∈G"  "b∈G"  "c∈G"  "d∈G"
    using OrderedGroup_ZF_1_L4 by auto
  with A2 have "a⋅c \<ls> a⋅d" 
    using group_strict_ord_transl_inv by simp
  moreover from ordGroupAssum A1 T have "a⋅d \<lsq> b⋅d"
     using IsAnOrdGroup_def by simp
   ultimately show "a⋅c \<ls> b⋅d"
     by (rule OrderedGroup_ZF_1_L4A)
qed

subsection‹The set of positive elements›

text‹In this section we study ‹G+› - the set of elements that are 
  (strictly) greater than the unit. The most important result is that every
  linearly ordered group can decomposed into $\{1\}$, ‹G+› and the 
  set of those elements $a\in G$ such that $a^{-1}\in$‹G+›. 
  Another property of linearly ordered groups that we prove here is that 
  if ‹G+›$\neq \emptyset$, then it is infinite. This allows to show 
  that nontrivial linearly ordered groups are infinite.›

text‹The positive set is closed under the group operation.›

lemma (in group3) OrderedGroup_ZF_1_L13: shows "G+ {is closed under} P"
proof -
  { fix a b assume "a∈G+"  "b∈G+"
    then have T1: "𝟭 \<lsq> a⋅b"   and "𝟭 ≠ a⋅b"
      using PositiveSet_def OrderedGroup_ZF_1_L11 OrderedGroup_ZF_1_L12
      by auto
    moreover from T1 have "a⋅b ∈ G"
      using OrderedGroup_ZF_1_L4 by simp
    ultimately have "a⋅b ∈ G+" using PositiveSet_def by simp
  } then show "G+ {is closed under} P" using IsOpClosed_def
    by simp
qed

text‹For totally ordered groups every nonunit element is positive or its 
  inverse is positive.›

lemma (in group3) OrderedGroup_ZF_1_L14:
  assumes A1: "r {is total on} G" and A2: "a∈G" 
  shows "a=𝟭 ∨ a∈G+ ∨ a¯∈G+"
proof -
  { assume A3: "a≠𝟭"
    moreover from A1 A2 have "a\<lsq>𝟭 ∨ 𝟭\<lsq>a"
      using IsTotal_def OrderedGroup_ZF_1_L1 group0.group0_2_L2
      by simp
    moreover from A3 A2 have T1: "a¯ ≠ 𝟭"
      using OrderedGroup_ZF_1_L1 group0.group0_2_L8B
      by simp
    ultimately have "a¯∈G+ ∨ a∈G+"
      using OrderedGroup_ZF_1_L5A OrderedGroup_ZF_1_L2A
      by auto
  } thus "a=𝟭 ∨ a∈G+ ∨ a¯∈G+" by auto
qed

text‹If an element belongs to the positive set, then it is not the unit
  and its inverse does not belong to the positive set.›

lemma (in group3) OrderedGroup_ZF_1_L15:
   assumes A1: "a∈G+"  shows "a≠𝟭"  "a¯∉G+"
proof -
  from A1 show T1: "a≠𝟭" using PositiveSet_def by auto
  { assume "a¯ ∈ G+" 
    with A1 have "a\<lsq>𝟭"  "𝟭\<lsq>a"
      using OrderedGroup_ZF_1_L5AA PositiveSet_def by auto
    then have "a=𝟭" by (rule group_order_antisym)
    with T1 have False by simp
  } then show "a¯∉G+" by auto
qed

text‹If $a^{-1}$ is positive, then $a$ can not be positive or the unit.›

lemma (in group3) OrderedGroup_ZF_1_L16:
  assumes A1: "a∈G" and A2: "a¯∈G+" shows "a≠𝟭"  "a∉G+"
proof -
  from A2 have "a¯≠𝟭"  "(a¯)¯ ∉ G+"
    using OrderedGroup_ZF_1_L15 by auto
  with A1 show "a≠𝟭"  "a∉G+"
    using OrderedGroup_ZF_1_L1 group0.group0_2_L8C group0.group_inv_of_inv 
    by auto
qed

text‹For linearly ordered groups each element is either the unit, 
  positive or its inverse is positive.›

lemma (in group3) OrdGroup_decomp: 
  assumes A1: "r {is total on} G" and A2: "a∈G" 
  shows "Exactly_1_of_3_holds (a=𝟭,a∈G+,a¯∈G+)"
proof -
  from A1 A2 have "a=𝟭 ∨ a∈G+ ∨ a¯∈G+"
    using OrderedGroup_ZF_1_L14 by simp
  moreover from A2 have "a=𝟭 ⟶ (a∉G+ ∧ a¯∉G+)"
    using OrderedGroup_ZF_1_L1 group0.group_inv_of_one
    PositiveSet_def by simp
  moreover from A2 have "a∈G+ ⟶ (a≠𝟭 ∧ a¯∉G+)"
    using OrderedGroup_ZF_1_L15 by simp
  moreover from A2 have "a¯∈G+ ⟶ (a≠𝟭 ∧ a∉G+)"
    using OrderedGroup_ZF_1_L16 by simp
  ultimately show "Exactly_1_of_3_holds (a=𝟭,a∈G+,a¯∈G+)"
    by (rule Fol1_L5)
qed

text‹A if $a$ is a nonunit element that is not positive, then $a^{-1}$ is 
  is positive. This is useful for some proofs by cases.›

lemma (in group3) OrdGroup_cases:
  assumes A1: "r {is total on} G" and A2: "a∈G" 
  and A3: "a≠𝟭"  "a∉G+"
  shows "a¯ ∈ G+"
proof -
  from A1 A2 have "a=𝟭 ∨ a∈G+ ∨ a¯∈G+"
    using OrderedGroup_ZF_1_L14 by simp
  with A3 show "a¯ ∈ G+" by auto
qed
  
text‹Elements from $G\setminus G_+$ are not greater that the unit.›

lemma (in group3) OrderedGroup_ZF_1_L17:
  assumes A1: "r {is total on} G" and A2: "a ∈ G-G+"
  shows "a\<lsq>𝟭"
proof -
  { assume "a=𝟭"
    with A2 have "a\<lsq>𝟭" using OrderedGroup_ZF_1_L3 by simp }
  moreover
  { assume "a≠𝟭"
    with A1 A2 have "a\<lsq>𝟭" 
      using PositiveSet_def OrderedGroup_ZF_1_L8A
      by auto }
  ultimately show "a\<lsq>𝟭" by auto
qed

text‹The next lemma allows to split proofs that something holds 
  for all $a\in G$ into cases $a=1$, $a\in G_+$, $-a\in G_+$.›

lemma (in group3) OrderedGroup_ZF_1_L18: 
  assumes A1: "r {is total on} G" and A2: "b∈G"
  and A3: "Q(𝟭)" and A4: "∀a∈G+. Q(a)" and A5: "∀a∈G+. Q(a¯)"
  shows "Q(b)"
proof -
  from A1 A2 A3 A4 A5 have "Q(b) ∨ Q((b¯)¯)"
    using OrderedGroup_ZF_1_L14 by auto
  with A2 show "Q(b)" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
    by simp
qed

text‹All elements greater or equal than an element of ‹G+›
  belong to ‹G+›.›

lemma (in group3) OrderedGroup_ZF_1_L19:
  assumes A1: "a ∈ G+" and A2: "a\<lsq>b"
  shows "b ∈ G+"
proof -
  from A1 have I: "𝟭\<lsq>a"  and II: "a≠𝟭"
    using OrderedGroup_ZF_1_L2A by auto
  from I A2 have "𝟭\<lsq>b" by (rule Group_order_transitive)
  moreover have "b≠𝟭"
  proof -
    { assume "b=𝟭"
      with I A2 have "𝟭\<lsq>a"  "a\<lsq>𝟭"
	by auto
      then have "𝟭=a" by (rule group_order_antisym)
      with II have False by simp
    } then show "b≠𝟭" by auto
  qed
  ultimately show "b ∈ G+" 
    using OrderedGroup_ZF_1_L2A by simp
qed

text‹The inverse of an element of ‹G+› cannot be in ‹G+›.›

lemma (in group3) OrderedGroup_ZF_1_L20:
  assumes A1: "r {is total on} G" and A2: "a ∈ G+" 
  shows "a¯ ∉ G+"
proof -
  from A2 have "a∈G" using PositiveSet_def
    by simp
  with A1 have "Exactly_1_of_3_holds (a=𝟭,a∈G+,a¯∈G+)"
    using OrdGroup_decomp by simp
  with A2 show "a¯ ∉ G+" by (rule Fol1_L7)
qed

text‹The set of positive elements of a 
  nontrivial linearly ordered group is not empty.›

lemma (in group3) OrderedGroup_ZF_1_L21:
  assumes A1: "r {is total on} G" and A2: "G ≠ {𝟭}"
  shows "G+ ≠ 0"
proof -
  have "𝟭 ∈ G" using OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by simp
  with A2 obtain a where "a∈G"  "a≠𝟭" by auto
  with A1 have "a∈G+ ∨ a¯∈G+" 
    using OrderedGroup_ZF_1_L14 by auto
  then show "G+ ≠ 0" by auto
qed

text‹If $b\in$‹G+›, then $a < a\cdot b$. 
  Multiplying $a$ by a positive elemnt increases $a$.›

lemma (in group3) OrderedGroup_ZF_1_L22:
  assumes A1: "a∈G"  "b∈G+"
  shows "a\<lsq>a⋅b"  "a ≠ a⋅b"  "a⋅b ∈ G"
proof -
  from ordGroupAssum A1 have "a⋅𝟭 \<lsq> a⋅b"
    using OrderedGroup_ZF_1_L2A IsAnOrdGroup_def
    by simp
  with A1 show "a\<lsq>a⋅b" 
    using OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by simp
  then show "a⋅b ∈ G"
    using OrderedGroup_ZF_1_L4 by simp
  { from A1 have "a∈G"  "b∈G"  
      using PositiveSet_def by auto
    moreover assume "a = a⋅b"
    ultimately have "b = 𝟭"
      using OrderedGroup_ZF_1_L1 group0.group0_2_L7
      by simp
    with A1 have False using PositiveSet_def
      by simp
  } then show "a ≠ a⋅b" by auto
qed

text‹If $G$ is a nontrivial linearly ordered hroup, 
  then for every element of $G$ we can find one in ‹G+› that is
  greater or equal.›

lemma (in group3) OrderedGroup_ZF_1_L23: 
  assumes A1: "r {is total on} G" and A2: "G ≠ {𝟭}"
  and A3: "a∈G"
  shows "∃b∈G+. a\<lsq>b"
proof -
  { assume A4: "a∈G+" then have "a\<lsq>a"
      using PositiveSet_def OrderedGroup_ZF_1_L3
      by simp
    with A4 have "∃b∈G+. a\<lsq>b" by auto }
  moreover
  { assume "a∉G+"
    with A1 A3 have I: "a\<lsq>𝟭" using OrderedGroup_ZF_1_L17
      by simp
    from A1 A2 obtain b where II: "b∈G+" 
      using OrderedGroup_ZF_1_L21 by auto
    then have "𝟭\<lsq>b" using PositiveSet_def by simp
    with I have "a\<lsq>b" by (rule Group_order_transitive)
    with II have "∃b∈G+. a\<lsq>b" by auto }
  ultimately show ?thesis by auto
qed

text‹The ‹G+› is ‹G+› plus the unit.›
lemma (in group3) OrderedGroup_ZF_1_L24: shows "G+ = G+∪{𝟭}"
  using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_1_L2A OrderedGroup_ZF_1_L3A
  by auto

text‹What is $-G_+$, really?›

lemma (in group3) OrderedGroup_ZF_1_L25: shows 
  "(\<sm>G+) = {a¯. a∈G+}"
  "(\<sm>G+) ⊆ G"
proof -
  from ordGroupAssum have I: "GroupInv(G,P) : G→G"
    using IsAnOrdGroup_def group0_2_T2 by simp
  moreover have "G+ ⊆ G" using PositiveSet_def by auto
  ultimately show 
    "(\<sm>G+) = {a¯. a∈G+}"
    "(\<sm>G+) ⊆ G"
    using func_imagedef func1_1_L6 by auto
qed

text‹If the inverse of $a$ is in ‹G+›, then $a$ is in the inverse
  of ‹G+›.›

lemma (in group3) OrderedGroup_ZF_1_L26:
  assumes A1: "a∈G" and A2: "a¯ ∈ G+"
  shows "a ∈ (\<sm>G+)"
proof -
  from A1 have "a¯ ∈ G"  "a = (a¯)¯" using OrderedGroup_ZF_1_L1 
    group0.inverse_in_group group0.group_inv_of_inv
    by auto
  with A2 show "a ∈ (\<sm>G+)" using OrderedGroup_ZF_1_L25
    by auto
qed

text‹If $a$ is in the inverse of  ‹G+›, 
  then its inverse is in $G_+$.›

lemma (in group3) OrderedGroup_ZF_1_L27:
  assumes "a ∈ (\<sm>G+)"
  shows "a¯ ∈ G+"
  using assms OrderedGroup_ZF_1_L25 PositiveSet_def 
    OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
  by auto

text‹A linearly ordered group can be decomposed into $G_+$, $\{1\}$ and
  $-G_+$›

lemma (in group3) OrdGroup_decomp2: 
  assumes A1: "r {is total on} G"
  shows 
  "G = G+ ∪ (\<sm>G+)∪ {𝟭}"
  "G+∩(\<sm>G+) = 0"
  "𝟭 ∉ G+∪(\<sm>G+)"
proof -
  { fix a assume A2: "a∈G"
    with A1 have "a∈G+ ∨ a¯∈G+ ∨ a=𝟭"
      using OrderedGroup_ZF_1_L14 by auto
    with A2 have "a∈G+ ∨ a∈(\<sm>G+) ∨ a=𝟭"
      using OrderedGroup_ZF_1_L26 by auto
    then have "a ∈ (G+ ∪ (\<sm>G+)∪ {𝟭})"
      by auto
  } then have "G ⊆ G+ ∪ (\<sm>G+)∪ {𝟭}"
    by auto
  moreover have "G+ ∪ (\<sm>G+)∪ {𝟭} ⊆ G"
    using OrderedGroup_ZF_1_L25 PositiveSet_def
      OrderedGroup_ZF_1_L1 group0.group0_2_L2
    by auto
  ultimately show "G = G+ ∪ (\<sm>G+)∪ {𝟭}" by auto
  { let ?A = "G+∩(\<sm>G+)"
    assume "G+∩(\<sm>G+) ≠ 0"
    then have "?A≠0" by simp
    then obtain a where "a∈?A" by blast
    then have False using OrderedGroup_ZF_1_L15 OrderedGroup_ZF_1_L27
      by auto
  } then show "G+∩(\<sm>G+) = 0" by auto
  show "𝟭 ∉ G+∪(\<sm>G+)"
    using OrderedGroup_ZF_1_L27
      OrderedGroup_ZF_1_L1 group0.group_inv_of_one
      OrderedGroup_ZF_1_L2A by auto
qed

text‹If $a\cdot b^{-1}$ is nonnegative, then $b \leq a$. This maybe used to
  recover the order from the set of nonnegative elements and serve as a way
  to define order by prescibing that set (see the "Alternative definitions"
  section).›

lemma (in group3) OrderedGroup_ZF_1_L28:
  assumes A1: "a∈G"  "b∈G" and A2: "a⋅b¯ ∈ G+"
  shows "b\<lsq>a"
proof -
  from A2 have "𝟭 \<lsq> a⋅b¯" using OrderedGroup_ZF_1_L2
    by simp
  with A1 show "b\<lsq>a" using OrderedGroup_ZF_1_L5K
    by simp
qed

text‹A special case of ‹OrderedGroup_ZF_1_L28› when
  $a\cdot b^{-1}$ is positive.›

corollary (in group3) OrderedGroup_ZF_1_L29:
  assumes A1: "a∈G"  "b∈G" and A2: "a⋅b¯ ∈ G+"
  shows "b\<lsq>a"  "b≠a"
proof -
  from A2 have "𝟭 \<lsq> a⋅b¯" and I: "a⋅b¯ ≠ 𝟭"
    using OrderedGroup_ZF_1_L2A by auto
  with A1 show "b\<lsq>a" using OrderedGroup_ZF_1_L5K
    by simp
  from A1 I show "b≠a" 
    using OrderedGroup_ZF_1_L1 group0.group0_2_L6
    by auto
qed

text‹A bit stronger that ‹OrderedGroup_ZF_1_L29›, adds
   case when two elements are equal.›

lemma (in group3) OrderedGroup_ZF_1_L30:
  assumes "a∈G"  "b∈G" and "a=b ∨ b⋅a¯ ∈ G+"
  shows "a\<lsq>b"
  using assms OrderedGroup_ZF_1_L3 OrderedGroup_ZF_1_L29
  by auto

text‹A different take on decomposition: we can have $a=b$ or $a<b$
  or $b<a$.›

lemma (in group3) OrderedGroup_ZF_1_L31: 
  assumes A1: "r {is total on} G" and A2: "a∈G"  "b∈G"
  shows "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
proof -
  from A2 have "a⋅b¯ ∈ G" using OrderedGroup_ZF_1_L1
    group0.inverse_in_group group0.group_op_closed
    by simp
  with A1 have "a⋅b¯ = 𝟭 ∨ a⋅b¯ ∈ G+ ∨ (a⋅b¯)¯ ∈ G+"
    using OrderedGroup_ZF_1_L14 by simp
  moreover
  { assume "a⋅b¯ = 𝟭"
    then have "a⋅b¯⋅b = 𝟭⋅b" by simp
    with A2 have "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
      using OrderedGroup_ZF_1_L1
	group0.inv_cancel_two group0.group0_2_L2 by auto }
  moreover
  { assume "a⋅b¯ ∈ G+"
    with A2 have "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
      using OrderedGroup_ZF_1_L29 by auto }
  moreover
  { assume "(a⋅b¯)¯ ∈ G+"
    with A2 have "b⋅a¯ ∈ G+" using OrderedGroup_ZF_1_L1
      group0.group0_2_L12 by simp
    with A2 have "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
      using OrderedGroup_ZF_1_L29 by auto }
  ultimately show "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
    by auto
qed

subsection‹Intervals and bounded sets›

text‹Intervals here are the closed intervals of the form 
 $\{x\in G. a\leq x \leq b \}$.›

text‹A bounded set can be translated to put it in  $G^+$ and then it is 
 still bounded above.›

lemma (in group3) OrderedGroup_ZF_2_L1: 
  assumes A1: "∀g∈A. L\<lsq>g ∧ g\<lsq>M"
  and A2: "S = RightTranslation(G,P,L¯)" 
  and A3: "a ∈ S``(A)"
  shows "a \<lsq> M⋅L¯"   "𝟭\<lsq>a"
proof -
  from A3 have "A≠0" using func1_1_L13A by fast
  then obtain g where "g∈A" by auto
  with A1 have T1: "L∈G" "M∈G" "L¯∈G" 
    using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 
    group0.inverse_in_group by auto
  with A2 have "S : G→G" using OrderedGroup_ZF_1_L1 group0.group0_5_L1
    by simp
  moreover from A1 have T2: "A⊆G" using OrderedGroup_ZF_1_L4 by auto
  ultimately have "S``(A) = {S`(b). b∈A}" using func_imagedef
    by simp
  with A3 obtain b where T3: "b∈A" "a = S`(b)" by auto
  with A1 ordGroupAssum T1 have "b⋅L¯\<lsq>M⋅L¯" "L⋅L¯\<lsq>b⋅L¯"
    using IsAnOrdGroup_def by auto
  with T3 A2 T1 T2 show "a\<lsq>M⋅L¯" "𝟭\<lsq>a"
    using OrderedGroup_ZF_1_L1 group0.group0_5_L2 group0.group0_2_L6 
    by auto
qed

text‹Every bounded set is an image of a subset of an interval that starts at 
  $1$.›

lemma (in group3) OrderedGroup_ZF_2_L2:
  assumes A1: "IsBounded(A,r)" 
  shows "∃B.∃g∈G+.∃T∈G→G. A = T``(B) ∧ B ⊆ Interval(r,𝟭,g)"
proof - 
  { assume A2: "A=0" 
    let ?B = "0"
    let ?g = "𝟭"
    let ?T = "ConstantFunction(G,𝟭)"
    have "?g∈G+" using OrderedGroup_ZF_1_L3A by simp
    moreover have "?T : G→G"
      using func1_3_L1 OrderedGroup_ZF_1_L1 group0.group0_2_L2 by simp
    moreover from A2 have "A = T``(?B)" by simp
    moreover have "?B ⊆ Interval(r,𝟭,?g)" by simp
    ultimately have
      "∃B.∃g∈G+.∃T∈G→G. A = T``(B) ∧ B ⊆ Interval(r,𝟭,g)"
      by auto }
  moreover
  { assume A3: "A≠0"
    with A1 have "∃L. ∀x∈A. L\<lsq>x" and "∃U. ∀x∈A. x\<lsq>U"
      using IsBounded_def IsBoundedBelow_def IsBoundedAbove_def 
      by auto
    then obtain L U where D1: "∀x∈A. L\<lsq>x ∧ x\<lsq>U "
      by auto
    with A3 have T1: "A⊆G" using OrderedGroup_ZF_1_L4 by auto
    from A3 obtain a where "a∈A" by auto
    with D1 have T2: "L\<lsq>a" "a\<lsq>U" by auto
    then have T3: "L∈G" "L¯∈ G" "U∈G" 
      using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 
	group0.inverse_in_group by auto
    let ?T = "RightTranslation(G,P,L)"
    let ?B = "RightTranslation(G,P,L¯)``(A)"
    let ?g = "U⋅L¯"
    have "?g∈G+"
    proof -
      from T2 have "L\<lsq>U" using Group_order_transitive by fast
      with ordGroupAssum T3 have "L⋅L¯\<lsq>?g" 
	using IsAnOrdGroup_def by simp
      with T3 show ?thesis using OrderedGroup_ZF_1_L1 group0.group0_2_L6
	OrderedGroup_ZF_1_L2 by simp
    qed
    moreover from T3 have "?T : G→G"
      using OrderedGroup_ZF_1_L1 group0.group0_5_L1
      by simp
    moreover have "A = ?T``(?B)"
    proof -
      from T3 T1 have "?T``(?B) = {a⋅L¯⋅L. a∈A}"
	using OrderedGroup_ZF_1_L1 group0.group0_5_L6
	by simp
      moreover from T3 T1 have "∀a∈A. a⋅L¯⋅L = a⋅(L¯⋅L)"
	using OrderedGroup_ZF_1_L1 group0.group_oper_assoc by auto
      ultimately have "?T``(?B) = {a⋅(L¯⋅L). a∈A}" by simp
      with T3 have "?T``(?B) = {a⋅𝟭. a∈A}"
	using OrderedGroup_ZF_1_L1 group0.group0_2_L6 by simp
      moreover from T1 have "∀a∈A. a⋅𝟭=a"
	using OrderedGroup_ZF_1_L1 group0.group0_2_L2 by auto
      ultimately show ?thesis by simp
    qed
    moreover have "?B ⊆ Interval(r,𝟭,?g)"
    proof
      fix y assume A4: "y ∈ ?B"
      let ?S = "RightTranslation(G,P,L¯)"
      from D1 have T4: "∀x∈A. L\<lsq>x ∧ x\<lsq>U" by simp
      moreover have T5: "?S = RightTranslation(G,P,L¯)" 
	by simp 
      moreover from A4 have T6: "y ∈ ?S``(A)" by simp
      ultimately have "y\<lsq>U⋅L¯" using OrderedGroup_ZF_2_L1
	by blast
      moreover from T4 T5 T6 have "𝟭\<lsq>y" by (rule OrderedGroup_ZF_2_L1)
      ultimately show "y ∈ Interval(r,𝟭,?g)" using Interval_def by auto
    qed
    ultimately have
      "∃B.∃g∈G+.∃T∈G→G. A = T``(B) ∧ B ⊆ Interval(r,𝟭,g)"
      by auto }
  ultimately show ?thesis by auto
qed
      
text‹If every interval starting at $1$ is finite, then every bounded set is 
  finite. I find it interesting that this does not require the group to be 
  linearly ordered (the order to be total).›

theorem (in group3) OrderedGroup_ZF_2_T1:
  assumes A1: "∀g∈G+. Interval(r,𝟭,g) ∈ Fin(G)"
  and A2: "IsBounded(A,r)" 
  shows "A ∈ Fin(G)"
proof -
  from A2 have
    "∃B.∃g∈G+.∃T∈G→G. A = T``(B) ∧ B ⊆ Interval(r,𝟭,g)"
    using OrderedGroup_ZF_2_L2 by simp
  then obtain B g T where D1: "g∈G+" "B ⊆ Interval(r,𝟭,g)" 
    and D2: "T : G→G" "A = T``(B)" by auto
  from D1 A1 have "B∈Fin(G)" using Fin_subset_lemma by blast
  with D2 show ?thesis using Finite1_L6A by simp
qed

text‹In linearly ordered groups finite sets are bounded.›

theorem (in group3) ord_group_fin_bounded:
  assumes "r {is total on} G" and "B∈Fin(G)" 
  shows "IsBounded(B,r)"
  using ordGroupAssum assms IsAnOrdGroup_def IsPartOrder_def Finite_ZF_1_T1
  by simp

text‹For nontrivial linearly ordered groups  if for every element $G$ 
  we can find one in $A$ 
  that is greater or equal (not necessarily strictly greater), then $A$
  can neither be finite nor bounded above.›

lemma (in group3) OrderedGroup_ZF_2_L2A:
  assumes A1: "r {is total on} G" and A2: "G ≠ {𝟭}"
  and A3: "∀a∈G. ∃b∈A. a\<lsq>b"
  shows 
  "∀a∈G. ∃b∈A. a≠b ∧ a\<lsq>b"
  "¬IsBoundedAbove(A,r)"
  "A ∉ Fin(G)"
proof -
  { fix a
    from A1 A2 obtain c where "c ∈ G+"
      using OrderedGroup_ZF_1_L21 by auto
    moreover assume "a∈G"
    ultimately have 
      "a⋅c ∈ G"  and I: "a \<ls> a⋅c"
      using OrderedGroup_ZF_1_L22 by auto
    with A3 obtain b where II: "b∈A"  and III: "a⋅c \<lsq> b"
      by auto
    moreover from I III have "a\<ls>b" by (rule OrderedGroup_ZF_1_L4A)
    ultimately have "∃b∈A. a≠b ∧ a\<lsq>b" by auto
  } thus "∀a∈G. ∃b∈A. a≠b ∧ a\<lsq>b" by simp
  with ordGroupAssum A1 show 
    "¬IsBoundedAbove(A,r)"
    "A ∉ Fin(G)"
    using IsAnOrdGroup_def IsPartOrder_def 
    OrderedGroup_ZF_1_L1A Order_ZF_3_L14 Finite_ZF_1_1_L3
    by auto
qed


text‹Nontrivial linearly ordered groups are infinite. Recall 
  that ‹Fin(A)› is the collection of finite subsets of $A$. 
  In this lemma we show that $G\notin$ ‹Fin(G)›, that is that
  $G$ is not a finite subset of itself. This is a way of saying that $G$ 
  is infinite. We also show that for nontrivial linearly ordered groups 
  ‹G+› is infinite.›

theorem (in group3) Linord_group_infinite:
  assumes A1: "r {is total on} G" and A2: "G ≠ {𝟭}"
  shows 
  "G+ ∉ Fin(G)"
  "G ∉ Fin(G)"
proof -
  from A1 A2 show I: "G+ ∉ Fin(G)"
    using OrderedGroup_ZF_1_L23 OrderedGroup_ZF_2_L2A
    by simp
  { assume "G ∈ Fin(G)"
    moreover have "G+ ⊆ G" using PositiveSet_def by auto
    ultimately have "G+ ∈ Fin(G)" using Fin_subset_lemma
      by blast
    with I have False by simp
  } then show "G ∉ Fin(G)" by auto
qed
  
text‹A property of nonempty subsets of linearly ordered groups that don't
  have a maximum: for any element in such subset we can find one that
  is strictly greater.›

lemma (in group3) OrderedGroup_ZF_2_L2B:
  assumes A1: "r {is total on} G" and A2: "A⊆G" and 
  A3: "¬HasAmaximum(r,A)" and A4: "x∈A"
  shows "∃y∈A. x\<ls>y"
proof -
  from ordGroupAssum assms have
    "antisym(r)"
    "r {is total on} G"
    "A⊆G"  "¬HasAmaximum(r,A)"  "x∈A"
    using IsAnOrdGroup_def IsPartOrder_def
    by auto
  then have "∃y∈A. ⟨x,y⟩ ∈ r ∧ y≠x"
    using Order_ZF_4_L16 by simp
  then show "∃y∈A. x\<ls>y" by auto
qed
    
text‹In linearly ordered groups $G\setminus G_+$ is bounded above.›

lemma (in group3) OrderedGroup_ZF_2_L3:
  assumes A1: "r {is total on} G" shows "IsBoundedAbove(G-G+,r)"
proof -
  from A1 have "∀a∈G-G+. a\<lsq>𝟭"
    using OrderedGroup_ZF_1_L17 by simp
  then show "IsBoundedAbove(G-G+,r)" 
    using IsBoundedAbove_def by auto
qed

text‹In linearly ordered groups if $A\cap G_+$ is finite, 
  then $A$ is bounded above.›

lemma (in group3) OrderedGroup_ZF_2_L4:
  assumes A1: "r {is total on} G" and A2: "A⊆G" 
  and A3: "A ∩ G+ ∈ Fin(G)"
  shows "IsBoundedAbove(A,r)"
proof -
  have "A ∩ (G-G+) ⊆ G-G+" by auto
  with A1 have "IsBoundedAbove(A ∩ (G-G+),r)"
    using OrderedGroup_ZF_2_L3 Order_ZF_3_L13
    by blast
  moreover from A1 A3 have "IsBoundedAbove(A ∩ G+,r)"
    using ord_group_fin_bounded IsBounded_def 
    by simp
  moreover from A1 ordGroupAssum have
    "r {is total on} G"  "trans(r)"  "r⊆G×G"
    using IsAnOrdGroup_def IsPartOrder_def by auto
  ultimately have "IsBoundedAbove(A ∩ (G-G+) ∪ A ∩ G+,r)"
    using Order_ZF_3_L3 by simp
  moreover from A2 have "A = A ∩ (G-G+) ∪ A ∩ G+"
    by auto
  ultimately show  "IsBoundedAbove(A,r)" by simp
qed

text‹If a set $-A\subseteq G$ is bounded above, then $A$ is bounded below.›

lemma (in group3) OrderedGroup_ZF_2_L5:
  assumes A1: "A⊆G" and A2: "IsBoundedAbove(\<sm>A,r)"
  shows "IsBoundedBelow(A,r)"
proof -
  { assume "A = 0" then have "IsBoundedBelow(A,r)"
      using IsBoundedBelow_def by auto }
  moreover
  { assume A3: "A≠0"
    from ordGroupAssum have I: "GroupInv(G,P) : G→G"
      using IsAnOrdGroup_def group0_2_T2 by simp
    with A1 A2 A3 obtain u where D: "∀a∈(\<sm>A). a\<lsq>u"
      using func1_1_L15A IsBoundedAbove_def by auto
    { fix b assume "b∈A"
      with A1 I D have "b¯ \<lsq> u" and T: "b∈G"
	using func_imagedef by auto
      then have "u¯\<lsq>(b¯)¯" using OrderedGroup_ZF_1_L5
	by simp
      with T have "u¯\<lsq>b"
	using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
	by simp
    } then have "∀b∈A. ⟨u¯,b⟩ ∈ r" by simp
    then have "IsBoundedBelow(A,r)"
      using Order_ZF_3_L9 by blast }
  ultimately show ?thesis by auto
qed

text‹If $a\leq b$, then the image of the interval $a..b$ by any function is
  nonempty.›

lemma (in group3) OrderedGroup_ZF_2_L6: 
  assumes "a\<lsq>b" and "f:G→G"
  shows "f``(Interval(r,a,b)) ≠ 0"
  using ordGroupAssum assms OrderedGroup_ZF_1_L4 
    Order_ZF_2_L6 Order_ZF_2_L2A 
    IsAnOrdGroup_def IsPartOrder_def func1_1_L15A
  by auto
  
end