Require Import Arith Omega.

Lemma nat_eq_or : forall n m:nat, n = m \/ n <> m.
Proof. intros n m; case (eq_nat_dec n m); auto. Qed.

Lemma eq_unique : forall n1 n2:nat, forall h1 h2: n1 = n2, h1 = h2.
Proof. apply Eqdep_dec.eq_proofs_unicity; exact nat_eq_or. Qed.

Scheme le_ind2 := Induction for le Sort Prop.
Lemma le_unique : forall m k, forall h g : m <= k, h = g.
Proof.
intros m k; change (forall h g, h = (eq_ind k (le m) g k (eq_refl k))).
induction h as [ | n h IH] using le_ind2; intros g.
 generalize g (eq_refl m); clear g; generalize m at 2 3 8; intros p g. 
 case g; [ |intros q l e; now case (le_Sn_n q); rewrite e].
 now intros e; rewrite (eq_unique _ _ e (eq_refl _)); simpl.
generalize g (eq_refl (S n)); generalize (S n) at 1 2 5; clear g.
intros p [ | q g] e; [case (le_Sn_n n); rewrite <- e; assumption| ].
generalize e g; injection e; intros f; rewrite f; clear e f g q; intros e g.
now rewrite (eq_unique _ _ e (eq_refl _)), (IH g).
Qed.