[STATEMENT]
lemma "K \<in> normal \<Longrightarrow> K \<in> convex \<Longrightarrow> K \<in> lsubgroup \<Longrightarrow> F K \<in> normalfilters"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> F K \<in> normalfilters
[PROOF STEP]
apply (rule lemma_3_10_ii_i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> F K \<in> filters
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> \<forall>a. {a} ** F K = F K ** {a}
[PROOF STEP]
apply (subgoal_tac "K \<in> subgroup")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup\<rbrakk> \<Longrightarrow> F K \<in> filters
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> \<forall>a. {a} ** F K = F K ** {a}
[PROOF STEP]
apply (subst filters_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup\<rbrakk> \<Longrightarrow> F K \<in> {F. F \<noteq> {} \<and> (\<forall>a b. a \<in> F \<and> b \<in> F \<longrightarrow> a * b \<in> F) \<and> (\<forall>a b. a \<in> F \<and> a \<le> b \<longrightarrow> b \<in> F)}
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> \<forall>a. {a} ** F K = F K ** {a}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; F K = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; b \<in> F K\<rbrakk> \<Longrightarrow> a * b \<in> F K
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subgoal_tac "1 \<in> F K")
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; F K = {}; 1 \<in> F K\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; F K = {}\<rbrakk> \<Longrightarrow> 1 \<in> F K
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; b \<in> F K\<rbrakk> \<Longrightarrow> a * b \<in> F K
 4. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 5. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 7. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; F K = {}\<rbrakk> \<Longrightarrow> 1 \<in> F K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; b \<in> F K\<rbrakk> \<Longrightarrow> a * b \<in> F K
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subst F_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; F K = {}\<rbrakk> \<Longrightarrow> 1 \<in> {a. u - Rep_G a \<in> K}
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; b \<in> F K\<rbrakk> \<Longrightarrow> a * b \<in> F K
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; F K = {}\<rbrakk> \<Longrightarrow> u - Rep_G 1 \<in> K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; b \<in> F K\<rbrakk> \<Longrightarrow> a * b \<in> F K
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subst one_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; F K = {}\<rbrakk> \<Longrightarrow> u - Rep_G (Abs_G u) \<in> K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; b \<in> F K\<rbrakk> \<Longrightarrow> a * b \<in> F K
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; b \<in> F K\<rbrakk> \<Longrightarrow> a * b \<in> F K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: F_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<in> K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: convex_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; \<forall>a b. a \<in> K \<and> b \<in> K \<longrightarrow> |[ a , b ]| \<subseteq> K; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<in> K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (drule_tac x = 0 in spec)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; \<forall>b. (0::'a) \<in> K \<and> b \<in> K \<longrightarrow> |[ 0::'a , b ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<in> K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (drule_tac x = "(u - Rep_G b) + (u - Rep_G a) " in spec)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; (0::'a) \<in> K \<and> u - Rep_G b + (u - Rep_G a) \<in> K \<longrightarrow> |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<in> K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<in> K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subgoal_tac "u - Rep_G (a * b) \<in> |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]|")
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]| \<subseteq> K; u - Rep_G (a * b) \<in> |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]|\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<in> K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<in> |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]|
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<in> |[ 0::'a , u - Rep_G b + (u - Rep_G a) ]|
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: closed_interval_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> (0::'a) \<le> u - Rep_G (a * b) \<and> u - Rep_G (a * b) \<le> u - Rep_G b + (u - Rep_G a)
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> (0::'a) \<le> u - Rep_G (a * b)
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<le> u - Rep_G b + (u - Rep_G a)
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (cut_tac x = "a * b" in Rep_G)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K; Rep_G (a * b) \<in> G\<rbrakk> \<Longrightarrow> (0::'a) \<le> u - Rep_G (a * b)
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<le> u - Rep_G b + (u - Rep_G a)
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: G_def diff_minus)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u + - Rep_G a \<in> K; u + - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u + - Rep_G b + (u + - Rep_G a)} \<subseteq> K; (0::'a) \<le> Rep_G (a * b) \<and> Rep_G (a * b) \<le> u\<rbrakk> \<Longrightarrow> (0::'a) \<le> u + - Rep_G (a * b)
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<le> u - Rep_G b + (u - Rep_G a)
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u + - Rep_G a \<in> K; u + - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u + - Rep_G b + (u + - Rep_G a)} \<subseteq> K; (0::'a) \<le> Rep_G (a * b) \<and> Rep_G (a * b) \<le> u\<rbrakk> \<Longrightarrow> (0::'a) + - (- Rep_G (a * b)) \<le> u
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<le> u - Rep_G b + (u - Rep_G a)
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G (a * b) \<le> u - Rep_G b + (u - Rep_G a)
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: times_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> (u - (Rep_G a - u + Rep_G b)) \<sqinter> u \<le> u - Rep_G b + (u - Rep_G a)
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subgoal_tac "(u - (Rep_G a - u + Rep_G b)) = u - Rep_G b + (u - Rep_G a)")
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K; u - (Rep_G a - u + Rep_G b) = u - Rep_G b + (u - Rep_G a)\<rbrakk> \<Longrightarrow> (u - (Rep_G a - u + Rep_G b)) \<sqinter> u \<le> u - Rep_G b + (u - Rep_G a)
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> u - (Rep_G a - u + Rep_G b) = u - Rep_G b + (u - Rep_G a)
 3. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 4. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 6. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; u - Rep_G b \<in> K; {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G b + (u - Rep_G a)} \<subseteq> K\<rbrakk> \<Longrightarrow> u - (Rep_G a - u + Rep_G b) = u - Rep_G b + (u - Rep_G a)
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: diff_minus add.assoc minus_add)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> F K
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subst (asm) Rep_G_order)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; a \<in> F K; Rep_G a \<le> Rep_G b\<rbrakk> \<Longrightarrow> b \<in> F K
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: F_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> K
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subst (asm) convex_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> {A. \<forall>a b. a \<in> A \<and> b \<in> A \<longrightarrow> |[ a , b ]| \<subseteq> A}; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> K
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; \<forall>a b. a \<in> K \<and> b \<in> K \<longrightarrow> |[ a , b ]| \<subseteq> K; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> K
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (drule_tac x = 0 in spec)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; \<forall>b. (0::'a) \<in> K \<and> b \<in> K \<longrightarrow> |[ 0::'a , b ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> K
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (drule_tac x = " u - Rep_G a" in spec)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; (0::'a) \<in> K \<and> u - Rep_G a \<in> K \<longrightarrow> |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> K
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> K
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subgoal_tac "u - Rep_G b \<in> |[ 0::'a , u - Rep_G a ]|")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K; u - Rep_G b \<in> |[ 0::'a , u - Rep_G a ]|\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> K
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> |[ 0::'a , u - Rep_G a ]|
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> |[ 0::'a , u - Rep_G a ]|
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (subst closed_interval_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<in> {c. (0::'a) \<le> c \<and> c \<le> u - Rep_G a}
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (0::'a) \<le> u - Rep_G b \<and> u - Rep_G b \<le> u - Rep_G a
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> (0::'a) \<le> u - Rep_G b
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<le> u - Rep_G a
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (cut_tac x = "b" in Rep_G)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K; Rep_G b \<in> G\<rbrakk> \<Longrightarrow> (0::'a) \<le> u - Rep_G b
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<le> u - Rep_G a
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K; (0::'a) \<le> Rep_G b \<and> Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'a) \<le> u - Rep_G b
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<le> u - Rep_G a
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (safe)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K; (0::'a) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'a) \<le> u - Rep_G b
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<le> u - Rep_G a
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: diff_minus)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u + - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u + - Rep_G a ]| \<subseteq> K; (0::'a) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'a) \<le> u + - Rep_G b
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<le> u - Rep_G a
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u + - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u + - Rep_G a ]| \<subseteq> K; (0::'a) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'a) + - (- Rep_G b) \<le> u
 2. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<le> u - Rep_G a
 3. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u - Rep_G b \<le> u - Rep_G a
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: diff_minus)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u + - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u + - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> u + - Rep_G b \<le> u + - Rep_G a
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (rule add_order_preserving_left)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u + - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u + - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> - Rep_G b \<le> - Rep_G a
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (rule minus_order)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>K \<in> normal; K \<in> lsubgroup; K \<in> subgroup; u + - Rep_G a \<in> K; Rep_G a \<le> Rep_G b; |[ 0::'a , u + - Rep_G a ]| \<subseteq> K\<rbrakk> \<Longrightarrow> - (- Rep_G a) \<le> - (- Rep_G b)
 2. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup\<rbrakk> \<Longrightarrow> K \<in> subgroup
 2. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (simp add: lsubgroup_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
 2. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (rule normal_1)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> K \<in> normal
 2. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> K \<in> convex
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> K \<in> lsubgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> {a} ** F K\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
 5. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> {a} ** F K
[PROOF STEP]
apply (rule normal_2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> K \<in> normal
 2. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> K \<in> convex
 3. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> K \<in> lsubgroup
 4. \<And>a x. \<lbrakk>K \<in> normal; K \<in> convex; K \<in> lsubgroup; x \<in> F K ** {a}\<rbrakk> \<Longrightarrow> x \<in> F K ** {a}
[PROOF STEP]
by simp_all


[STATEMENT]
lemma [simp]: "Rep_N a + Rep_N b \<in> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a + Rep_N b \<in> N
[PROOF STEP]
apply (cut_tac x = a in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<in> N \<Longrightarrow> Rep_N a + Rep_N b \<in> N
[PROOF STEP]
apply (cut_tac x = b in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_N a \<in> N; Rep_N b \<in> N\<rbrakk> \<Longrightarrow> Rep_N a + Rep_N b \<in> N
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_N a \<le> (0::'b); Rep_N b \<le> (0::'b)\<rbrakk> \<Longrightarrow> Rep_N a + Rep_N b \<le> (0::'b)
[PROOF STEP]
apply (rule_tac left_move_to_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_N a \<le> (0::'b); Rep_N b \<le> (0::'b)\<rbrakk> \<Longrightarrow> Rep_N b \<le> - Rep_N a + (0::'b)
[PROOF STEP]
apply (rule_tac y = 0 in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_N a \<le> (0::'b); Rep_N b \<le> (0::'b)\<rbrakk> \<Longrightarrow> Rep_N b \<le> (0::'b)
 2. \<lbrakk>Rep_N a \<le> (0::'b); Rep_N b \<le> (0::'b)\<rbrakk> \<Longrightarrow> (0::'b) \<le> - Rep_N a + (0::'b)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_N a \<le> (0::'b); Rep_N b \<le> (0::'b)\<rbrakk> \<Longrightarrow> (0::'b) \<le> - Rep_N a
[PROOF STEP]
apply (rule_tac minus_order)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_N a \<le> (0::'b); Rep_N b \<le> (0::'b)\<rbrakk> \<Longrightarrow> - (- Rep_N a) \<le> - (0::'b)
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "inf (Rep_N b - Rep_N a) 0 \<in> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b - Rep_N a) \<sqinter> (0::'b) \<in> N
[PROOF STEP]
apply (cut_tac x = a in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<in> N \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'b) \<in> N
[PROOF STEP]
apply (cut_tac x = b in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_N a \<in> N; Rep_N b \<in> N\<rbrakk> \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'b) \<in> N
[PROOF STEP]
by (simp add: N_def)


[STATEMENT]
lemma [simp]: "inf (- Rep_N a + Rep_N b) 0 \<in> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N a + Rep_N b) \<sqinter> (0::'b) \<in> N
[PROOF STEP]
apply (cut_tac x = a in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<in> N \<Longrightarrow> (- Rep_N a + Rep_N b) \<sqinter> (0::'b) \<in> N
[PROOF STEP]
apply (cut_tac x = b in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_N a \<in> N; Rep_N b \<in> N\<rbrakk> \<Longrightarrow> (- Rep_N a + Rep_N b) \<sqinter> (0::'b) \<in> N
[PROOF STEP]
by (simp add: N_def)


[STATEMENT]
lemma [simp]: "0 \<in> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'b) \<in> N
[PROOF STEP]
by (simp add: N_def)


[STATEMENT]
lemma order_Rep_N:
  "((a::'a N) \<le> b) = (Rep_N a \<le> Rep_N b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b) = (Rep_N a \<le> Rep_N b)
[PROOF STEP]
apply (subst order_N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b = 1) = (Rep_N a \<le> Rep_N b)
[PROOF STEP]
apply (simp add: impl_N_def one_N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N a \<le> Rep_N b)
[PROOF STEP]
apply (subgoal_tac "(Abs_N (inf (Rep_N b - Rep_N a) (0::'a)) = Abs_N (0::'a)) = ((Rep_N (Abs_N (inf (Rep_N b - Rep_N a) (0::'a))) = Rep_N(Abs_N (0::'a))))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))) \<Longrightarrow> (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N a \<le> Rep_N b)
 2. (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))) \<Longrightarrow> (Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))) = (Rep_N a \<le> Rep_N b)
 2. (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> (Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))) = (Rep_N a \<le> Rep_N b)
 2. (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
[PROOF STEP]
apply (simp add: Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a)) = (Rep_N a \<le> Rep_N b)
 2. (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> Rep_N a \<le> Rep_N b
 2. Rep_N a \<le> Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a)
 3. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 4. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subgoal_tac "0 \<le> Rep_N b - Rep_N a")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a); (0::'a) \<le> Rep_N b - Rep_N a\<rbrakk> \<Longrightarrow> Rep_N a \<le> Rep_N b
 2. (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (0::'a) \<le> Rep_N b - Rep_N a
 3. Rep_N a \<le> Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a)
 4. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 5. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (drule_tac v = "Rep_N a" in add_order_preserving_right)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a); (0::'a) + Rep_N a \<le> Rep_N b - Rep_N a + Rep_N a\<rbrakk> \<Longrightarrow> Rep_N a \<le> Rep_N b
 2. (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (0::'a) \<le> Rep_N b - Rep_N a
 3. Rep_N a \<le> Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a)
 4. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 5. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (simp add: diff_minus add.assoc)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (0::'a) \<le> Rep_N b - Rep_N a
 2. Rep_N a \<le> Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a)
 3. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 4. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (rule_tac y = "inf (Rep_N b - Rep_N a) (0::'a)" in order_trans)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (0::'a) \<le> (Rep_N b - Rep_N a) \<sqinter> (0::'a)
 2. (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) \<le> Rep_N b - Rep_N a
 3. Rep_N a \<le> Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a)
 4. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 5. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) \<le> Rep_N b - Rep_N a
 2. Rep_N a \<le> Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a)
 3. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 4. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. True \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) \<le> Rep_N b - Rep_N a
 2. Rep_N a \<le> Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a)
 3. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 4. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N a \<le> Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) = (0::'a)
 2. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 3. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Rep_N a \<le> Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a) \<sqinter> (0::'a) \<le> (0::'a)
 2. Rep_N a \<le> Rep_N b \<Longrightarrow> (0::'a) \<le> (Rep_N b - Rep_N a) \<sqinter> (0::'a)
 3. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 4. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N a \<le> Rep_N b \<Longrightarrow> (0::'a) \<le> (Rep_N b - Rep_N a) \<sqinter> (0::'a)
 2. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 3. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N a \<le> Rep_N b \<Longrightarrow> (0::'a) \<le> Rep_N b - Rep_N a
 2. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 3. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (simp add: diff_minus)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N a \<le> Rep_N b \<Longrightarrow> (0::'a) \<le> Rep_N b + - Rep_N a
 2. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 3. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N a \<le> Rep_N b \<Longrightarrow> (0::'a) + - (- Rep_N a) \<le> Rep_N b
 2. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 3. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a) \<Longrightarrow> Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 2. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)) \<Longrightarrow> Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
by (simp add: Abs_N_inverse)


[STATEMENT]
lemma order_Abs_N:
  "a \<in> N \<Longrightarrow> b \<in> N \<Longrightarrow> (a \<le> b) = (Abs_N a \<le> Abs_N b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (a \<le> b) = (Abs_N a \<le> Abs_N b)
[PROOF STEP]
apply (subst order_N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (a \<le> b) = (Abs_N a l\<rightarrow> Abs_N b = 1)
[PROOF STEP]
apply (simp add: impl_N_def one_N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (a \<le> b) = (Abs_N ((Rep_N (Abs_N b) - Rep_N (Abs_N a)) \<sqinter> (0::'a)) = Abs_N (0::'a))
[PROOF STEP]
apply (simp add: Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (a \<le> b) = (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a))
[PROOF STEP]
apply (subgoal_tac "inf (b - a) 0 \<in> N")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N\<rbrakk> \<Longrightarrow> (a \<le> b) = (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a))
 2. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (subgoal_tac "(Abs_N (inf (b - a) (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N (inf (b - a) (0::'a))) = Rep_N (Abs_N (0::'a)))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))\<rbrakk> \<Longrightarrow> (a \<le> b) = (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a))
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N\<rbrakk> \<Longrightarrow> (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))\<rbrakk> \<Longrightarrow> (a \<le> b) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N\<rbrakk> \<Longrightarrow> (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (simp add: Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = ((b - a) \<sqinter> (0::'a) = (0::'a))\<rbrakk> \<Longrightarrow> (a \<le> b) = ((b - a) \<sqinter> (0::'a) = (0::'a))
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N\<rbrakk> \<Longrightarrow> (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = ((b - a) \<sqinter> (0::'a) = (0::'a)); True\<rbrakk> \<Longrightarrow> (a \<le> b) = ((b - a) \<sqinter> (0::'a) = (0::'a))
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N\<rbrakk> \<Longrightarrow> (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(b - a) \<sqinter> (0::'a) \<in> N; (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = ((b - a) \<sqinter> (0::'a) = (0::'a)); True; True\<rbrakk> \<Longrightarrow> (a \<le> b) = ((b - a) \<sqinter> (0::'a) = (0::'a))
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N\<rbrakk> \<Longrightarrow> (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = ((b - a) \<sqinter> (0::'a) = (0::'a)); True; True; True\<rbrakk> \<Longrightarrow> (a \<le> b) = ((b - a) \<sqinter> (0::'a) = (0::'a))
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N\<rbrakk> \<Longrightarrow> (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>True; True; True; True\<rbrakk> \<Longrightarrow> (a \<le> b) = ((b - a) \<sqinter> (0::'a) = (0::'a))
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N\<rbrakk> \<Longrightarrow> (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a \<le> b) = ((b - a) \<sqinter> (0::'a) = (0::'a))
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N\<rbrakk> \<Longrightarrow> (Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)) = (Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a)))
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. a \<le> b \<Longrightarrow> (b - a) \<sqinter> (0::'a) = (0::'a)
 2. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> a \<le> b
 3. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)\<rbrakk> \<Longrightarrow> Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 4. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 5. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. a \<le> b \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<le> (0::'a)
 2. a \<le> b \<Longrightarrow> (0::'a) \<le> (b - a) \<sqinter> (0::'a)
 3. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> a \<le> b
 4. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)\<rbrakk> \<Longrightarrow> Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))
 5. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 6. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a \<le> b \<Longrightarrow> (0::'a) \<le> b - a
 2. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> a \<le> b
 3. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 4. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (simp add: diff_minus)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a \<le> b \<Longrightarrow> (0::'a) \<le> b + - a
 2. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> a \<le> b
 3. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 4. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a \<le> b \<Longrightarrow> (0::'a) + - (- a) \<le> b
 2. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> a \<le> b
 3. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 4. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> a \<le> b
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (subgoal_tac "0 \<le> b - a")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(b - a) \<sqinter> (0::'a) = (0::'a); (0::'a) \<le> b - a\<rbrakk> \<Longrightarrow> a \<le> b
 2. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (0::'a) \<le> b - a
 3. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 4. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (drule_tac v = "a" in add_order_preserving_right)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(b - a) \<sqinter> (0::'a) = (0::'a); (0::'a) + a \<le> b - a + a\<rbrakk> \<Longrightarrow> a \<le> b
 2. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (0::'a) \<le> b - a
 3. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 4. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (simp add: diff_minus add.assoc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (0::'a) \<le> b - a
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (rule_tac y = "inf (b - a) (0::'a)" in order_trans)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (0::'a) \<le> (b - a) \<sqinter> (0::'a)
 2. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<le> b - a
 3. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 4. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (b - a) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<le> b - a
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. True \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<le> b - a
 2. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 3. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> N; b \<in> N; (b - a) \<sqinter> (0::'a) \<in> N; Rep_N (Abs_N ((b - a) \<sqinter> (0::'a))) = Rep_N (Abs_N (0::'a))\<rbrakk> \<Longrightarrow> Abs_N ((b - a) \<sqinter> (0::'a)) = Abs_N (0::'a)
 2. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
apply (simp add: Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> N; b \<in> N\<rbrakk> \<Longrightarrow> (b - a) \<sqinter> (0::'a) \<in> N
[PROOF STEP]
by (simp add: N_def)


[STATEMENT]
lemma [simp]: "(1::'a N) * a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * a = a
[PROOF STEP]
by (simp add: one_N_def times_N_def Abs_N_inverse Rep_N_inverse)


[STATEMENT]
lemma [simp]: "a * (1::'a N) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * 1 = a
[PROOF STEP]
by (simp add: one_N_def times_N_def Abs_N_inverse Rep_N_inverse)


[STATEMENT]
lemma [simp]: "a l\<rightarrow> a = (1::'a N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a l\<rightarrow> a = 1
[PROOF STEP]
by (simp add: impl_N_def one_N_def Abs_N_inverse Rep_N_inverse)


[STATEMENT]
lemma [simp]: "a r\<rightarrow> a = (1::'a N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a r\<rightarrow> a = 1
[PROOF STEP]
by (simp add: impr_N_def one_N_def Abs_N_inverse Rep_N_inverse)


[STATEMENT]
lemma impl_times: "(a l\<rightarrow> b) * a = (b l\<rightarrow> a) * (b::'a N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) * a = (b l\<rightarrow> a) * b
[PROOF STEP]
apply (simp add: impl_N_def impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (Rep_N b \<sqinter> Rep_N a) = Abs_N (Rep_N a \<sqinter> Rep_N b)
[PROOF STEP]
apply (subgoal_tac "inf (Rep_N b - Rep_N a + Rep_N a) (Rep_N a) = inf (Rep_N a - Rep_N b + Rep_N b) (Rep_N b)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N b - Rep_N a + Rep_N a) \<sqinter> Rep_N a = (Rep_N a - Rep_N b + Rep_N b) \<sqinter> Rep_N b \<Longrightarrow> Abs_N (Rep_N b \<sqinter> Rep_N a) = Abs_N (Rep_N a \<sqinter> Rep_N b)
 2. (Rep_N b - Rep_N a + Rep_N a) \<sqinter> Rep_N a = (Rep_N a - Rep_N b + Rep_N b) \<sqinter> Rep_N b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b - Rep_N a + Rep_N a) \<sqinter> Rep_N a = (Rep_N a - Rep_N b + Rep_N b) \<sqinter> Rep_N b
[PROOF STEP]
apply (subgoal_tac "Rep_N b - Rep_N a + Rep_N a = Rep_N b ")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b - Rep_N a + Rep_N a = Rep_N b \<Longrightarrow> (Rep_N b - Rep_N a + Rep_N a) \<sqinter> Rep_N a = (Rep_N a - Rep_N b + Rep_N b) \<sqinter> Rep_N b
 2. Rep_N b - Rep_N a + Rep_N a = Rep_N b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b \<sqinter> Rep_N a = Rep_N a \<sqinter> Rep_N b
 2. Rep_N b - Rep_N a + Rep_N a = Rep_N b
[PROOF STEP]
apply (subgoal_tac "Rep_N a - Rep_N b + Rep_N b = Rep_N a")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N a - Rep_N b + Rep_N b = Rep_N a \<Longrightarrow> Rep_N b \<sqinter> Rep_N a = Rep_N a \<sqinter> Rep_N b
 2. Rep_N a - Rep_N b + Rep_N b = Rep_N a
 3. Rep_N b - Rep_N a + Rep_N a = Rep_N b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N b \<sqinter> Rep_N a = Rep_N a \<sqinter> Rep_N b
 2. Rep_N a - Rep_N b + Rep_N b = Rep_N a
 3. Rep_N b - Rep_N a + Rep_N a = Rep_N b
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Rep_N b \<sqinter> Rep_N a \<le> Rep_N a \<sqinter> Rep_N b
 2. Rep_N a \<sqinter> Rep_N b \<le> Rep_N b \<sqinter> Rep_N a
 3. Rep_N a - Rep_N b + Rep_N b = Rep_N a
 4. Rep_N b - Rep_N a + Rep_N a = Rep_N b
[PROOF STEP]
by simp_all


[STATEMENT]
lemma impr_times: "a * (a r\<rightarrow> b) = (b::'a N) * (b r\<rightarrow> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (a r\<rightarrow> b) = b * (b r\<rightarrow> a)
[PROOF STEP]
apply (simp add: impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (Rep_N b \<sqinter> Rep_N a) = Abs_N (Rep_N a \<sqinter> Rep_N b)
[PROOF STEP]
apply (subgoal_tac "inf (Rep_N a + (- Rep_N a + Rep_N b)) (Rep_N a) = inf (Rep_N b + (- Rep_N b + Rep_N a)) (Rep_N b)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N a + (- Rep_N a + Rep_N b)) \<sqinter> Rep_N a = (Rep_N b + (- Rep_N b + Rep_N a)) \<sqinter> Rep_N b \<Longrightarrow> Abs_N (Rep_N b \<sqinter> Rep_N a) = Abs_N (Rep_N a \<sqinter> Rep_N b)
 2. (Rep_N a + (- Rep_N a + Rep_N b)) \<sqinter> Rep_N a = (Rep_N b + (- Rep_N b + Rep_N a)) \<sqinter> Rep_N b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N a + (- Rep_N a + Rep_N b)) \<sqinter> Rep_N a = (Rep_N b + (- Rep_N b + Rep_N a)) \<sqinter> Rep_N b
[PROOF STEP]
apply (simp add: add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N b \<sqinter> Rep_N a = Rep_N a \<sqinter> Rep_N b
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b \<sqinter> Rep_N a \<le> Rep_N a \<sqinter> Rep_N b
 2. Rep_N a \<sqinter> Rep_N b \<le> Rep_N b \<sqinter> Rep_N a
[PROOF STEP]
by simp_all


[STATEMENT]
lemma impr_impl_times: "(a l\<rightarrow> b) * a = (a::'a N) * (a r\<rightarrow> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) * a = a * (a r\<rightarrow> b)
[PROOF STEP]
by (simp add: impl_N_def impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)


[STATEMENT]
lemma impl_ded: "(a::'a N) * b l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
[PROOF STEP]
apply (simp add: impl_N_def impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a)) = Abs_N ((Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a))
[PROOF STEP]
apply (subgoal_tac "inf (Rep_N c - (Rep_N a + Rep_N b)) (0::'a) = inf (inf (Rep_N c - Rep_N b - Rep_N a) (- Rep_N a)) (0::'a)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) = (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<Longrightarrow> Abs_N ((Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a)) = Abs_N ((Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a))
 2. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) = (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) = (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a)
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a)
 2. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> Rep_N c - Rep_N b - Rep_N a \<and> (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> - Rep_N a
 2. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> Rep_N c - Rep_N b - Rep_N a
 2. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> - Rep_N a
 3. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply (rule_tac y = "Rep_N c - (Rep_N a + Rep_N b)" in order_trans)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
 2. Rep_N c - (Rep_N a + Rep_N b) \<le> Rep_N c - Rep_N b - Rep_N a
 3. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> - Rep_N a
 4. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N c - (Rep_N a + Rep_N b) \<le> Rep_N c - Rep_N b - Rep_N a
 2. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> - Rep_N a
 3. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply (simp add: diff_minus minus_add add.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> - Rep_N a
 2. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply (rule_tac y = "0" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (Rep_N c - (Rep_N a + Rep_N b)) \<sqinter> (0::'a) \<le> (0::'a)
 2. (0::'a) \<le> - Rep_N a
 3. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) \<le> - Rep_N a
 2. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply (cut_tac x = a in "Rep_N")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N a \<in> N \<Longrightarrow> (0::'a) \<le> - Rep_N a
 2. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N a \<le> (0::'a) \<Longrightarrow> (0::'a) \<le> - Rep_N a
 2. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply (drule_tac u = 0 and v = "- Rep_N a" in add_order_preserving)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) + Rep_N a + - Rep_N a \<le> (0::'a) + (0::'a) + - Rep_N a \<Longrightarrow> (0::'a) \<le> - Rep_N a
 2. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply (rule_tac y = "inf (Rep_N c - Rep_N b - Rep_N a) (- Rep_N a)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<sqinter> (0::'a) \<le> (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a
 2. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply (rule inf_le1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply (rule_tac y = "Rep_N c - Rep_N b - Rep_N a" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c - Rep_N b - Rep_N a) \<sqinter> - Rep_N a \<le> Rep_N c - Rep_N b - Rep_N a
 2. Rep_N c - Rep_N b - Rep_N a \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N c - Rep_N b - Rep_N a \<le> Rep_N c - (Rep_N a + Rep_N b)
[PROOF STEP]
by (simp add: diff_minus minus_add add.assoc)


[STATEMENT]
lemma impr_ded: "(a::'a N) * b r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b r\<rightarrow> c = b r\<rightarrow> a r\<rightarrow> c
[PROOF STEP]
apply (simp add: impr_N_def impr_N_def times_N_def Abs_N_inverse Rep_N_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a)) = Abs_N ((- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a))
[PROOF STEP]
apply (subgoal_tac "inf (- (Rep_N a + Rep_N b) + Rep_N c) (0::'a) = inf (inf (- Rep_N b + (- Rep_N a + Rep_N c)) (- Rep_N b)) (0::'a)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) = (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<Longrightarrow> Abs_N ((- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a)) = Abs_N ((- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a))
 2. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) = (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) = (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a)
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a)
 2. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N b + (- Rep_N a + Rep_N c) \<and> (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N b
 2. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N b + (- Rep_N a + Rep_N c)
 2. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N b
 3. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply (rule_tac y = "- (Rep_N a + Rep_N b) + Rep_N c" in order_trans)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
 2. - (Rep_N a + Rep_N b) + Rep_N c \<le> - Rep_N b + (- Rep_N a + Rep_N c)
 3. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N b
 4. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. - (Rep_N a + Rep_N b) + Rep_N c \<le> - Rep_N b + (- Rep_N a + Rep_N c)
 2. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N b
 3. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply (simp add: diff_minus minus_add add.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N b
 2. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply (rule_tac y = "0" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (- (Rep_N a + Rep_N b) + Rep_N c) \<sqinter> (0::'a) \<le> (0::'a)
 2. (0::'a) \<le> - Rep_N b
 3. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) \<le> - Rep_N b
 2. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply (cut_tac x = b in "Rep_N")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b \<in> N \<Longrightarrow> (0::'a) \<le> - Rep_N b
 2. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b \<le> (0::'a) \<Longrightarrow> (0::'a) \<le> - Rep_N b
 2. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply (drule_tac u = 0 and v = "- Rep_N b" in add_order_preserving)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) + Rep_N b + - Rep_N b \<le> (0::'a) + (0::'a) + - Rep_N b \<Longrightarrow> (0::'a) \<le> - Rep_N b
 2. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply (rule_tac y = "inf (- Rep_N b + (- Rep_N a + Rep_N c)) (- Rep_N b)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<sqinter> (0::'a) \<le> (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b
 2. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply (rule inf_le1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply (rule_tac y = "- Rep_N b + (- Rep_N a + Rep_N c)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N b + (- Rep_N a + Rep_N c)) \<sqinter> - Rep_N b \<le> - Rep_N b + (- Rep_N a + Rep_N c)
 2. - Rep_N b + (- Rep_N a + Rep_N c) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Rep_N b + (- Rep_N a + Rep_N c) \<le> - (Rep_N a + Rep_N b) + Rep_N c
[PROOF STEP]
by (simp add: diff_minus minus_add add.assoc)


[STATEMENT]
lemma Rep_N_inf: "Rep_N ((a::'a::lgroup N) \<sqinter> b) = (Rep_N a) \<sqinter> (Rep_N b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N (a \<sqinter> b) = Rep_N a \<sqinter> Rep_N b
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N (a \<sqinter> b) \<le> Rep_N a \<sqinter> Rep_N b
 2. Rep_N a \<sqinter> Rep_N b \<le> Rep_N (a \<sqinter> b)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N (a \<sqinter> b) \<le> Rep_N a \<and> Rep_N (a \<sqinter> b) \<le> Rep_N b
 2. Rep_N a \<sqinter> Rep_N b \<le> Rep_N (a \<sqinter> b)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N (a \<sqinter> b) \<le> Rep_N a
 2. Rep_N (a \<sqinter> b) \<le> Rep_N b
 3. Rep_N a \<sqinter> Rep_N b \<le> Rep_N (a \<sqinter> b)
[PROOF STEP]
apply (simp add: order_Rep_N [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N (a \<sqinter> b) \<le> Rep_N b
 2. Rep_N a \<sqinter> Rep_N b \<le> Rep_N (a \<sqinter> b)
[PROOF STEP]
apply (simp add: order_Rep_N [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<sqinter> Rep_N b \<le> Rep_N (a \<sqinter> b)
[PROOF STEP]
apply (subgoal_tac "inf (Rep_N a) (Rep_N b) \<in> N")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Rep_N a \<sqinter> Rep_N b \<le> Rep_N (a \<sqinter> b)
 2. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply (subst order_Abs_N)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Rep_N a \<sqinter> Rep_N b \<in> N
 2. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Rep_N (a \<sqinter> b) \<in> N
 3. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> Abs_N (Rep_N (a \<sqinter> b))
 4. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Rep_N (a \<sqinter> b) \<in> N
 2. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> Abs_N (Rep_N (a \<sqinter> b))
 3. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply (cut_tac x = "a \<sqinter> b" in Rep_N)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Rep_N a \<sqinter> Rep_N b \<in> N; Rep_N (a \<sqinter> b) \<in> N\<rbrakk> \<Longrightarrow> Rep_N (a \<sqinter> b) \<in> N
 2. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> Abs_N (Rep_N (a \<sqinter> b))
 3. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> Abs_N (Rep_N (a \<sqinter> b))
 2. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply (simp add: Rep_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> a \<and> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> b
 2. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> a
 2. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> b
 3. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply (subst order_Rep_N)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Rep_N (Abs_N (Rep_N a \<sqinter> Rep_N b)) \<le> Rep_N a
 2. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> b
 3. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply (simp add: Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Abs_N (Rep_N a \<sqinter> Rep_N b) \<le> b
 2. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply (subst order_Rep_N)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<in> N \<Longrightarrow> Rep_N (Abs_N (Rep_N a \<sqinter> Rep_N b)) \<le> Rep_N b
 2. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply (simp add: Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<sqinter> Rep_N b \<in> N
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<sqinter> Rep_N b \<le> (0::'a)
[PROOF STEP]
apply (rule_tac y = "Rep_N a" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N a \<sqinter> Rep_N b \<le> Rep_N a
 2. Rep_N a \<le> (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<le> (0::'a)
[PROOF STEP]
apply (cut_tac x = a in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<in> N \<Longrightarrow> Rep_N a \<le> (0::'a)
[PROOF STEP]
by (simp add: N_def)


[STATEMENT]
lemma sup_inf_distrib2_lgroup: "(b \<sqinter> c) \<squnion> a = (b \<squnion> a) \<sqinter> (c \<squnion> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> c \<squnion> a = (b \<squnion> a) \<sqinter> (c \<squnion> a)
[PROOF STEP]
by (rule sup_inf_distrib2)


[STATEMENT]
lemma inf_sup_distrib2_lgroup: "(b \<squnion> c) \<sqinter> a = (b \<sqinter> a) \<squnion> (c \<sqinter> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<squnion> c) \<sqinter> a = b \<sqinter> a \<squnion> c \<sqinter> a
[PROOF STEP]
by (rule inf_sup_distrib2)


[STATEMENT]
lemma cancel_times_left: "(a::'a N) * b = a * c \<Longrightarrow> b = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b = a * c \<Longrightarrow> b = c
[PROOF STEP]
apply (simp add: times_N_def Abs_N_inverse Rep_N_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (Rep_N a + Rep_N b) = Abs_N (Rep_N a + Rep_N c) \<Longrightarrow> b = c
[PROOF STEP]
apply (subgoal_tac "Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Abs_N (Rep_N a + Rep_N b) = Abs_N (Rep_N a + Rep_N c); Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c))\<rbrakk> \<Longrightarrow> b = c
 2. Abs_N (Rep_N a + Rep_N b) = Abs_N (Rep_N a + Rep_N c) \<Longrightarrow> Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c))
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c)); True\<rbrakk> \<Longrightarrow> b = c
 2. Abs_N (Rep_N a + Rep_N b) = Abs_N (Rep_N a + Rep_N c) \<Longrightarrow> Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c))
[PROOF STEP]
apply (simp add: Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b = Rep_N c \<Longrightarrow> b = c
 2. Abs_N (Rep_N a + Rep_N b) = Abs_N (Rep_N a + Rep_N c) \<Longrightarrow> Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c))
[PROOF STEP]
apply (subgoal_tac "Abs_N (Rep_N b) = Abs_N (Rep_N c)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Rep_N b = Rep_N c; Abs_N (Rep_N b) = Abs_N (Rep_N c)\<rbrakk> \<Longrightarrow> b = c
 2. Rep_N b = Rep_N c \<Longrightarrow> Abs_N (Rep_N b) = Abs_N (Rep_N c)
 3. Abs_N (Rep_N a + Rep_N b) = Abs_N (Rep_N a + Rep_N c) \<Longrightarrow> Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c))
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Abs_N (Rep_N b) = Abs_N (Rep_N c); True\<rbrakk> \<Longrightarrow> b = c
 2. Rep_N b = Rep_N c \<Longrightarrow> Abs_N (Rep_N b) = Abs_N (Rep_N c)
 3. Abs_N (Rep_N a + Rep_N b) = Abs_N (Rep_N a + Rep_N c) \<Longrightarrow> Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c))
[PROOF STEP]
apply (simp add: Rep_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b = Rep_N c \<Longrightarrow> Abs_N (Rep_N b) = Abs_N (Rep_N c)
 2. Abs_N (Rep_N a + Rep_N b) = Abs_N (Rep_N a + Rep_N c) \<Longrightarrow> Rep_N (Abs_N (Rep_N a + Rep_N b)) = Rep_N (Abs_N (Rep_N a + Rep_N c))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma cancel_times_right: "b * (a::'a N) = c * a \<Longrightarrow> b = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * a = c * a \<Longrightarrow> b = c
[PROOF STEP]
apply (simp add: times_N_def Abs_N_inverse Rep_N_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (Rep_N b + Rep_N a) = Abs_N (Rep_N c + Rep_N a) \<Longrightarrow> b = c
[PROOF STEP]
apply (subgoal_tac "Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Abs_N (Rep_N b + Rep_N a) = Abs_N (Rep_N c + Rep_N a); Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a))\<rbrakk> \<Longrightarrow> b = c
 2. Abs_N (Rep_N b + Rep_N a) = Abs_N (Rep_N c + Rep_N a) \<Longrightarrow> Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a))
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a)); True\<rbrakk> \<Longrightarrow> b = c
 2. Abs_N (Rep_N b + Rep_N a) = Abs_N (Rep_N c + Rep_N a) \<Longrightarrow> Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a))
[PROOF STEP]
apply (simp add: Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b = Rep_N c \<Longrightarrow> b = c
 2. Abs_N (Rep_N b + Rep_N a) = Abs_N (Rep_N c + Rep_N a) \<Longrightarrow> Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a))
[PROOF STEP]
apply (subgoal_tac "Abs_N (Rep_N b) = Abs_N (Rep_N c)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Rep_N b = Rep_N c; Abs_N (Rep_N b) = Abs_N (Rep_N c)\<rbrakk> \<Longrightarrow> b = c
 2. Rep_N b = Rep_N c \<Longrightarrow> Abs_N (Rep_N b) = Abs_N (Rep_N c)
 3. Abs_N (Rep_N b + Rep_N a) = Abs_N (Rep_N c + Rep_N a) \<Longrightarrow> Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a))
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Abs_N (Rep_N b) = Abs_N (Rep_N c); True\<rbrakk> \<Longrightarrow> b = c
 2. Rep_N b = Rep_N c \<Longrightarrow> Abs_N (Rep_N b) = Abs_N (Rep_N c)
 3. Abs_N (Rep_N b + Rep_N a) = Abs_N (Rep_N c + Rep_N a) \<Longrightarrow> Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a))
[PROOF STEP]
apply (simp add: Rep_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b = Rep_N c \<Longrightarrow> Abs_N (Rep_N b) = Abs_N (Rep_N c)
 2. Abs_N (Rep_N b + Rep_N a) = Abs_N (Rep_N c + Rep_N a) \<Longrightarrow> Rep_N (Abs_N (Rep_N b + Rep_N a)) = Rep_N (Abs_N (Rep_N c + Rep_N a))
[PROOF STEP]
by simp_all