[STATEMENT]
lemma diff_hmem_imp_less: assumes "x \<^bold>\<in> y" shows "Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
have  "Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y
[PROOF STEP]
by (metis hdiff_iff hsubsetI hsubset_imp_le)
[PROOF STATE]
proof (state)
this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
have "Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<^bold>\<in> y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y
[PROOF STEP]
by (metis Rep_hf_inject hdiff_iff hinsert_iff)
[PROOF STATE]
proof (state)
this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y
Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y
Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
by (metis le_neq_implies_less)
[PROOF STATE]
proof (state)
this:
Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y

goal:
No subgoals!
[PROOF STEP]
qed