Require Import FMaps.
Require Import Arith.
Require Import EqNat.

Module NatOrd <: OrderedType.
  Definition t := nat.
  Definition eq (t1 t2 : t) : Prop:= eq_nat t1 t2.
  Definition lt (t1 t2 : t) : Prop:= lt t1 t2.
  Definition eq_dec (x y : t) := eq_nat_decide x y.

  Theorem eq_refl : forall y : t, eq y y.
    unfold eq; intro; apply eq_nat_refl.
  Qed.
  
  Theorem eq_sym : forall (y z: t), eq y z-> eq z y.
    unfold eq; intros.
    apply eq_eq_nat; apply sym_eq.
    apply eq_nat_eq; exact H.
  Qed.

  Theorem eq_trans : forall (w y z: t), eq w y -> eq y z -> eq w z.
    unfold eq; intros; rewrite (eq_nat_eq _ _ H); rewrite (eq_nat_eq _ _ H0); 
      exact (eq_refl z).
  Qed.
  Definition lt_trans : forall w y z : t, lt w y -> lt y z -> lt w z := lt_trans.
  
  Theorem lt_not_eq : forall (y z : t), lt y z ->~ eq y z.
    unfold eq; unfold lt; intros y z; case y; case z; try (simpl; auto).
    omega.
    unfold not; intros; generalize (eq_nat_eq _ _ H0); omega.
  Qed.
  
  Lemma compare : forall y z : t, Compare lt eq y z.
    intros.
    elim (le_lt_dec y z); intros.
    elim (eq_nat_dec y z); intros.
    rewrite a0.
    exact (EQ _ (eq_refl z)).
    assert (y < z).
    omega.
    exact (LT _ H).
    exact (GT _ b).
Qed.
End NatOrd.

Module NatMap := FMapList.Make (NatOrd).