Library Poset





Record Poset (A:Type) : Type := poset_constr 

{

 eq : A -> A -> Prop;

 eq_refl : forall x : A, eq x x;

 eq_sym : forall x y : A, eq x y -> eq y x;

 eq_trans : forall x y z : A, eq x y -> eq y z -> eq x z;




 order : A -> A -> Prop;

 order_refl : forall x y : A, eq x y -> order x y;

 order_antisym : forall x y : A, order x y -> order y x -> eq x y;

 order_trans : forall x y z : A, order x y -> order y z -> order x z

}.

Implicit Arguments order [A].

Implicit Arguments eq [A].

Implicit Arguments order_refl [A].

Implicit Arguments order_antisym [A].

Implicit Arguments order_trans [A].

Implicit Arguments eq_refl [A].

Implicit Arguments eq_sym [A].

Implicit Arguments eq_trans [A].




Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans.
Index
This page has been generated by coqdoc