diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 472489ff1f..9076f55427 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -206,12 +206,39 @@ protected inductive Lex : α × β → α × β → Prop where
   | left  {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : Prod.Lex (a₁, b₁) (a₂, b₂)
   | right (a) {b₁ b₂} (h : rb b₁ b₂)         : Prod.Lex (a, b₁)  (a, b₂)
 
+theorem lex_def (r : α → α → Prop) (s : β → β → Prop) {p q : α × β} :
+    Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2 :=
+  ⟨fun h => by cases h <;> simp [*], fun h =>
+    match p, q, h with
+    | (a, b), (c, d), Or.inl h => Lex.left _ _ h
+    | (a, b), (c, d), Or.inr ⟨e, h⟩ => by subst e; exact Lex.right _ h⟩
+
+namespace Lex
+
+instance [αeqDec : DecidableEq α] {r : α → α → Prop} [rDec : DecidableRel r]
+    {s : β → β → Prop} [sDec : DecidableRel s] : DecidableRel (Prod.Lex r s)
+  | (a, b), (a', b') =>
+    match rDec a a' with
+    | isTrue raa' => isTrue $ left b b' raa'
+    | isFalse nraa' =>
+      match αeqDec a a' with
+      | isTrue eq => by
+        subst eq
+        cases sDec b b' with
+        | isTrue sbb' => exact isTrue $ right a sbb'
+        | isFalse nsbb' =>
+          apply isFalse; intro contra; cases contra <;> contradiction
+      | isFalse neqaa' => by
+        apply isFalse; intro contra; cases contra <;> contradiction
+
 -- TODO: generalize
-def Lex.right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
+def right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
   match Nat.eq_or_lt_of_le h₁ with
   | Or.inl h => h ▸ Prod.Lex.right a₁ h₂
   | Or.inr h => Prod.Lex.left b₁ _ h
 
+end Lex
+
 -- relational product based on ra and rb
 inductive RProd : α × β → α × β → Prop where
   | intro {a₁ b₁ a₂ b₂} (h₁ : ra a₁ a₂) (h₂ : rb b₁ b₂) : RProd (a₁, b₁) (a₂, b₂)