# Library basis.ordered_set

``` Require Import Relations. Require Import Arith. Inductive comp : Set :=   | Equivalent : comp   | Less_than : comp   | Greater_than : comp   | Uncomparable : comp. Module Type S. Variable A : Set. Axiom eq_dec : forall e1 e2 : A, {e1 = e2} + {e1 <> e2}. Parameter o : relation A. Axiom o_proof : order A o. Axiom o_dec : forall e1 e2 : A, {o e1 e2} + {~ o e1 e2}. Axiom o_total : forall e1 e2 : A, {o e1 e2} + {o e2 e1}. End S. Module Type ES. Parameter A : Set. Parameter eq_A : relation A. Axiom eq_dec : forall a1 a2 : A, {eq_A a1 a2} + {~eq_A a1 a2}. Axiom eq_proof : equivalence A eq_A. Parameter o : relation A. Axiom o_compat :   forall e1 e1' e2 e2', eq_A e1 e1' -> eq_A e2 e2' -> o e1 e2 -> o e1' e2'. Axiom o_proof : order A o. Axiom o_dec : forall e1 e2 : A, {o e1 e2} + {~ o e1 e2}. Axiom o_total : forall e1 e2 : A, {o e1 e2} + {o e2 e1}.   Add Relation A eq_A   reflexivity proved by (equiv_refl _ _ eq_proof)     symmetry proved by (equiv_sym _ _ eq_proof)       transitivity proved by (equiv_trans _ _ eq_proof) as EQA. End ES. Module Nat <: S with Definition A:=nat. Definition A := nat. Definition o : relation A := le. Lemma o_proof : order A o. Proof. unfold o; constructor; auto. unfold reflexive; auto. unfold transitive; intros n1 n2 n3 H1 H2; apply le_trans with n2; trivial. unfold antisymmetric; auto with arith. Qed. Lemma o_dec : forall e1 e2 : A, {o e1 e2} + {~ o e1 e2}. Proof. unfold o. induction e1; induction e2. left; trivial. left; auto with arith. right; auto with arith. destruct (IHe1 e2); destruct IHe2; auto with arith. Defined. Lemma o_total : forall e1 e2 : A, {o e1 e2} + {o e2 e1}. Proof. intros. unfold o. change ({e1<=e2}+{e1>=e2}). apply le_ge_dec. Qed. Lemma eq_dec : forall e1 e2 : A, {e1 = e2}+{e1<>e2}. Proof. intros; decide equality. Defined. End Nat. ```