feat(order/rel_classes): any relation on an empty type is a well-order (

#14600)

src/logic/is_empty.lean

@@ -116,6 +116,9 @@ by simp only [← not_nonempty_iff, nonempty_sum, not_or_distrib]
 @[simp] lemma is_empty_psum {α β} : is_empty (psum α β) ↔ is_empty α ∧ is_empty β :=
 by simp only [← not_nonempty_iff, nonempty_psum, not_or_distrib]
 
+lemma well_founded_of_empty {α} [is_empty α] (r : α → α → Prop) : well_founded r :=
+⟨is_empty_elim⟩ 
+
 variables (α)
 
 lemma is_empty_or_nonempty : is_empty α ∨ nonempty α :=

src/order/rel_classes.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro, Yury G. Kudryashov
 -/
 import order.basic
+import logic.is_empty
 
 /-!
 # Unbundled relation classes
@@ -233,6 +234,13 @@ instance empty_relation.is_well_order [subsingleton α] : is_well_order α empty
   trans        := λ a b c, false.elim,
   wf           := ⟨λ a, ⟨_, λ y, false.elim⟩⟩ }
 
+@[priority 100]
+instance is_empty.is_well_order [is_empty α] (r : α → α → Prop) : is_well_order α r :=
+{ trichotomous := is_empty_elim,
+  irrefl       := is_empty_elim,
+  trans        := is_empty_elim,
+  wf           := well_founded_of_empty r }
+
 instance prod.lex.is_well_order [is_well_order α r] [is_well_order β s] :
   is_well_order (α × β) (prod.lex r s) :=
 { trichotomous := λ ⟨a₁, a₂⟩ ⟨b₁, b₂⟩,