proposition: Lemma le_unique : forall n m (h1 h2 : n <= m), h1 = h2.
proof: Proof. intro n. assert (forall m (h1 : n <= m) p (h2 : n <= p), m=p -> eq_dep nat (le n) m h1 p h2). intros m h1; elim h1 using le_ind_dep. intros p h2; case h2; intros. auto. subst n. absurd (S m0 <= m0); auto with arith. intros m0 l Hrec p h2. case h2; intros. subst n; absurd (S m0 <= m0); auto with arith. assert (m0=m1); auto ; subst m0. replace l0 with l; auto. apply (@eq_dep_eq _ eq_nat_dec (le n) m1); auto. intros; apply (@eq_dep_eq _ eq_nat_dec (le n) m); auto. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)