feat(order/basic): recursor for order_dual (#8938)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/order/basic.lean

@@ -174,6 +174,7 @@ def strict_mono_decr_on [has_lt α] [has_lt β] (f : α → β) (t : set α) : P
 def order_dual (α : Type*) : Type* := α
 
 namespace order_dual
+
 instance (α : Type*) [h : nonempty α] : nonempty (order_dual α) := h
 instance (α : Type*) [h : subsingleton α] : subsingleton (order_dual α) := h
 instance (α : Type*) [has_le α] : has_le (order_dual α) := ⟨λ x y : α, y ≤ x⟩

src/order/order_dual.lean

@@ -69,4 +69,9 @@ lemma to_dual_le [has_le α] {a : α} {b : order_dual α} :
 lemma to_dual_lt [has_lt α] {a : α} {b : order_dual α} :
   to_dual a < b ↔ of_dual b < a := iff.rfl
 
+/-- Recursor for `order_dual α`. -/
+@[elab_as_eliminator]
+protected def rec {C : order_dual α → Sort*} (h₂ : Π (a : α), C (to_dual a)) :
+  Π (a : order_dual α), C a := h₂
+
 end order_dual