[STATEMENT]
lemma sorted_list_of_set_insert_remove_cons:
  assumes "finite A" "less_sets {a} A"
  shows "sorted_list_of_set (insert a A) = a # sorted_list_of_set A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
have "strict_sorted (a # sorted_list_of_set A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_sorted (a # sorted_list_of_set A)
[PROOF STEP]
using assms less_setsD
[PROOF STATE]
proof (prove)
using this:
finite A
{a} \<lless> A
\<lbrakk>?A \<lless> ?B; ?a \<in> ?A; ?b \<in> ?B\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. strict_sorted (a # sorted_list_of_set A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strict_sorted (a # sorted_list_of_set A)

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
strict_sorted (a # sorted_list_of_set A)

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
have "list.set (a # sorted_list_of_set A) = insert a A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (a # sorted_list_of_set A) = insert a A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
{a} \<lless> A

goal (1 subgoal):
 1. list.set (a # sorted_list_of_set A) = insert a A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
list.set (a # sorted_list_of_set A) = insert a A

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list.set (a # sorted_list_of_set A) = insert a A

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
have "length (a # sorted_list_of_set A) = card (insert a A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (a # sorted_list_of_set A) = card (insert a A)
[PROOF STEP]
using assms card_insert_if less_setsD
[PROOF STATE]
proof (prove)
using this:
finite A
{a} \<lless> A
finite ?A \<Longrightarrow> card (insert ?x ?A) = (if ?x \<in> ?A then card ?A else Suc (card ?A))
\<lbrakk>?A \<lless> ?B; ?a \<in> ?A; ?b \<in> ?B\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. length (a # sorted_list_of_set A) = card (insert a A)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
length (a # sorted_list_of_set A) = card (insert a A)

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
strict_sorted (a # sorted_list_of_set A)
list.set (a # sorted_list_of_set A) = insert a A
length (a # sorted_list_of_set A) = card (insert a A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
strict_sorted (a # sorted_list_of_set A)
list.set (a # sorted_list_of_set A) = insert a A
length (a # sorted_list_of_set A) = card (insert a A)

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
by (metis \<open>finite A\<close> finite_insert sorted_list_of_set_unique)
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (insert a A) = a # sorted_list_of_set A

goal:
No subgoals!
[PROOF STEP]
qed