To try to understand how to define my own OrderedType in Coq, I'm working my way through the examples of OrderedTypes given in the standard library in Coq.Structures.OrderedTypeEx (here). As of right now I'm only concerned with the first couple of modules:
Require Import OrderedType.
Require Import ZArith.
Require Import Omega.
Require Import NArith Ndec.
Require Import Compare_dec.
Module Type UsualOrderedType.
Parameter Inline t : Type.
Definition eq := @eq t.
Parameter Inline lt : t -> t -> Prop.
Definition eq_refl := @eq_refl t.
Definition eq_sym := @eq_sym t.
Definition eq_trans := @eq_trans t.
Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Parameter compare : forall x y : t, Compare lt eq x y.
Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
End UsualOrderedType.
Module UOT_to_OT (U: UsualOrderedType) <: OrderedType := U.
Module Nat_as_OT <: UsualOrderedType.
Definition t := nat.
Definition eq := @eq nat.
Definition eq_refl := @eq_refl t.
Definition eq_sym := @eq_sym t.
Definition eq_trans := @eq_trans t.
Definition lt := lt.
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Definition compare x y : Compare lt eq x y.
Definition eq_dec := eq_nat_dec.
End Nat_as_OT.
When I step through this on my own in Proof General, I get the error Error: Proof editing in progress. When I get to last line. It appears that it wants me to prove lt_trans before it accepts that the module is over. That's fair enough. But how is this working as part of the standard library if the proof is not there? Is it implicitly referencing some prior proof in a way I don't understand? Additional, if I do Proof. Admitted. to be able to skip past the Lemma proofs, it then wants a proof for Definition compare x y : Compare lt eq x y.. Why would it ask for a proof for a definition?