proposition: Lemma le_unique : forall (x y : nat) (p q: x <= y), p = q.
proof: Proof. induction p using le_ind'; uniqueness 1; assert False by lia; intuition. Qed.
imports: Coq.Arith.Peano_dec Coq.Lists.SetoidList Lia Metalib.CoqUniquenessTac