[STATEMENT]
lemma not_weak_iff:
  assumes x: "x \<in> A" and y: "y \<in> A" shows "\<not> y \<sqsubseteq> x \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> y \<sqsubseteq> x) = (x \<sqsubseteq> y \<and> x \<noteq> y)
[PROOF STEP]
using x y
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A

goal (1 subgoal):
 1. (\<not> y \<sqsubseteq> x) = (x \<sqsubseteq> y \<and> x \<noteq> y)
[PROOF STEP]
by (cases rule: comparable_cases, auto intro:antisym)