proposition: Lemma le_eq : forall (x y:nat) (p1 p2: x <= y), p1 = p2.
proof: Proof. intros x y p1. elim p1 using le_rec. intros p2. destruct (@le_inversion x x p2) as [(x0,H0)|(x0,(x1,(x2,_)))]. rewrite H0. rewrite (eq_proofs_unicity nat_dec x0 (eq_refl x)); auto. subst. absurd (S x0 <= x0); auto with arith. intros. destruct (@le_inversion x (S m) p2) as [(x0,H0)|(x0,(x1,(x2,H0)))]. absurd (S m <= m); auto with arith. rewrite <- x0. assumption. injection x1; intros; subst. rewrite (H x2). rewrite (eq_proofs_unicity nat_dec x1 (eq_refl (S m))); auto. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)