proposition: Theorem NotInEqComp : forall (a b : A) (L : list A), ~ InEq a L -> eqA a b -> ~ InEq b L.
proof: Proof. intros a b L H' H'0; red in |- *; intros H'1; case H'; auto. apply InEqComp with (a := b); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)