(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                      A_decidable_total_ordering.v                        *)
(****************************************************************************)

(* G. Huet 1-9-95 *)

Require A_decidable.
Require A_total_ordering.

(* Some extra postulates which might prove useful somewhere
   but which are not needed for Heapsort *)

(* 
Axiom equ_tran : (x,y,z:A)(equ x y)->(equ y z)->(equ x z).
Axiom equ_refl : (x:A)(equ x x).

Axiom compat_inf_equ_right : (x,y,z:A)(inf x y)->(equ y z)->(inf x z).
Axiom compat_inf_equ_left  : (x,y,z:A)->(equ x y)(inf y z)->(inf x z).
Axiom antisym_inf_equ : (x,y:A)(inf x y)->(inf y x)->(equ x y)
*)



(* $Id: A_decidable_total_ordering.v,v 1.3 1998/04/30 16:45:56 mohring Exp $ *)
