Commit 0fdb55f6 authored by Björn Brandenburg's avatar Björn Brandenburg

add ltn_leq_trans utility lemma match leq_ltn_trans in ssrnat
parent 503b22a1
......@@ -105,3 +105,24 @@ Section NatLemmas.
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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment