chore(Order): deprecate gt_irrefl (#25567)

Author: JovanGerb

Mathlib/Order/Defs/PartialOrder.lean

@@ -81,7 +81,8 @@ alias LE.le.not_gt := not_lt_of_ge
 lemma ge_trans : a ≥ b → b ≥ c → a ≥ c := fun h₁ h₂ => le_trans h₂ h₁
 
 lemma lt_irrefl (a : α) : ¬a < a := fun h ↦ not_le_of_gt h le_rfl
-lemma gt_irrefl (a : α) : ¬a > a := lt_irrefl _
+
+@[deprecated (since := "2025-06-07")] alias gt_irrefl := lt_irrefl
 
 lemma lt_of_lt_of_le (hab : a < b) (hbc : b ≤ c) : a < c :=
   lt_of_le_not_ge (le_trans (le_of_lt hab) hbc) fun hca ↦ not_le_of_gt hab (le_trans hbc hca)