[STATEMENT]
lemma quasisym_not_greater:
  "cmp a b = Equiv" if "cmp a b \<noteq> Greater" and "cmp b a \<noteq> Greater"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmp a b = Equiv
[PROOF STEP]
using that comp.exhaust greater_iff_sym_less
[PROOF STATE]
proof (prove)
using this:
cmp a b \<noteq> Greater
cmp b a \<noteq> Greater
\<lbrakk>?y = Less \<Longrightarrow> ?P; ?y = Equiv \<Longrightarrow> ?P; ?y = Greater \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(cmp ?b ?a = Greater) = (cmp ?a ?b = Less)

goal (1 subgoal):
 1. cmp a b = Equiv
[PROOF STEP]
by auto