proposition: Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'.
proof: Proof. unfold eqk, ltk. unfold not. intros x x' H. destruct x, x'. simpl in *. intro. symmetry in H. apply lt_not_eq in H. auto. subst. auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses