+(* Constructions with nminus ************************************************)
+
+(*** monotonic_lt_minus_l *)
+lemma nlt_minus_sn_bi (o) (m) (n): o ≤ m → m < n → m - o < n - o.
+#o #m #n #Hom #Hmn
+lapply (nle_minus_sn_bi … o Hmn) -Hmn
+<(nminus_succ_sn … Hom) //
+qed.
+
+(* Destructions with nminus *************************************************)