diff --git a/util/nat.v b/util/nat.v
index 7cca339ef50b20361f3c5be1cbd8f6178de1b915..064d6e4b572ccdf9771107530d6b8c3200c98a7f 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -103,5 +103,26 @@ Section NatLemmas.
   Proof.
     intros* AC. ssromega.
   Qed.
-  
-End NatLemmas.
\ No newline at end of file
+
+End NatLemmas.
+
+Section NatOrderLemmas.
+
+  (* Mimic the way implicit arguments are used in ssreflect. *)
+  Set Implicit Arguments.
+  Unset Strict Implicit.
+
+  (* ltn_leq_trans: Establish that m < p if m < n and n <= p, to mirror the
+     lemma leq_ltn_trans in ssrnat.
+
+     NB: There is a good reason for this lemma to be "missing" in ssrnat --
+     since m < n is defined as m.+1 <= n, ltn_leq_trans is just
+     m.+1 <= n -> n <= p -> m.+1 <= p, that is (@leq_trans n m.+1 p).
+
+     Nonetheless we introduce it here because an additional (even though
+     arguably redundant) lemma doesn't hurt, and for newcomers the apparent
+     absence of the mirror case of leq_ltn_trans can be somewhat confusing.  *)
+  Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.
+  Proof. exact (@leq_trans n m.+1 p). Qed.
+
+End NatOrderLemmas.