[STATEMENT]
lemma pos_le_neg[simp]: "Pos A \<le> Neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pos A \<le> Neg A
[PROOF STEP]
unfolding less_eq_literal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atm_of (Pos A) < atm_of (Neg A) \<or> atm_of (Pos A) \<le> atm_of (Neg A) \<and> is_neg (Pos A) \<le> is_neg (Neg A)
[PROOF STEP]
by simp