diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
index cff09b9564d8aa..65b1ffe5e9eaca 100644
--- a/Mathlib/Order/Basic.lean
+++ b/Mathlib/Order/Basic.lean
@@ -191,6 +191,9 @@ theorem gt_imp_gt_of_le_of_le (h₁ : a ≤ c) (h₂ : d ≤ b) : a > b → c >
 
 attribute [gcongr strict] lt_of_lt_of_le lt_of_lt_of_le'
 
+@[to_dual (attr := gcongr strict) ge_imp_gt_of_lt']
+theorem ge_imp_gt_of_lt (h : a < b) : a ≥ c → b > c := lt_of_lt_of_le' h
+
 namespace Mathlib.Tactic.GCongr
 open Lean Meta
 
diff --git a/MathlibTest/Tactic/GRewrite.lean b/MathlibTest/Tactic/GRewrite.lean
index 62a69dee5f6a3f..06d0bbc0dad641 100644
--- a/MathlibTest/Tactic/GRewrite.lean
+++ b/MathlibTest/Tactic/GRewrite.lean
@@ -477,6 +477,12 @@ example (h₁ : a ≤ b) (h₂ : b < c) : a < c := by
 example (h₁ : a ≤ b) (h₂ : b < c) : a < c := by
   by_contra!; grw [← h₂, ← h₁] at this; contrapose! this; rfl
 
+example (h₁ : a < b) (h₂ : b ≤ c) : c > a := by
+  grw [h₁, h₂]
+
+example (h₁ : a < b) (h₂ : b ≤ c) : c > a := by
+  grw [← h₂, ← h₁]
+
 -- Strict inequalities can also be used as non-strict ones:
 example (h₁ : a < b) (h₂ : b < c) : a ≤ c := by
   grw [h₁, h₂]