chore(data/list): a list sorted w.r.t. (<) has no duplicates (#5550)

Author: urkud

src/data/list/nodup.lean

@@ -28,6 +28,10 @@ namespace list
 @[simp] theorem nodup_cons {a : α} {l : list α} : nodup (a::l) ↔ a ∉ l ∧ nodup l :=
 by simp only [nodup, pairwise_cons, forall_mem_ne]
 
+protected lemma pairwise.nodup {l : list α} {r : α → α → Prop} [is_irrefl α r] (h : pairwise r l) :
+  nodup l :=
+h.imp $ λ a b, ne_of_irrefl
+
 lemma rel_nodup {r : α → β → Prop} (hr : relator.bi_unique r) : (forall₂ r ⇒ (↔)) nodup nodup
 | _ _ forall₂.nil      := by simp only [nodup_nil]
 | _ _ (forall₂.cons hab h) :=

src/data/list/sort.lean

@@ -49,6 +49,10 @@ rel_of_pairwise_cons
   sorted r (a :: l) ↔ (∀ b ∈ l, r a b) ∧ sorted r l :=
 pairwise_cons
 
+protected theorem sorted.nodup {r : α → α → Prop} [is_irrefl α r] {l : list α} (h : sorted r l) :
+  nodup l :=
+h.nodup
+
 theorem eq_of_perm_of_sorted [is_antisymm α r]
   {l₁ l₂ : list α} (p : l₁ ~ l₂) (s₁ : sorted r l₁) (s₂ : sorted r l₂) : l₁ = l₂ :=
 begin

src/order/rel_classes.lean

@@ -83,6 +83,9 @@ instance [linear_order α] : is_trichotomous α (>) := is_trichotomous.swap _
 instance order_dual.is_total_le [has_le α] [is_total α (≤)] : is_total (order_dual α) (≤) :=
 @is_total.swap α _ _
 
+lemma ne_of_irrefl {r} [is_irrefl α r] : ∀ {x y : α}, r x y → x ≠ y
+| _ _ h rfl := irrefl _ h
+
 lemma trans_trichotomous_left [is_trans α r] [is_trichotomous α r] {a b c : α} :
   ¬r b a → r b c → r a c :=
 begin