+
+lemma nle_pred_sn (m) (n): m ≤ ↑n → ↓m ≤ n.
+#m #n elim m -m //
+/2 width=1 by nle_pred_bi/
+qed-.
+
+(* Destructions with npred **************************************************)
+
+lemma nle_inv_pred_sn (m) (n): ↓m ≤ n → m ≤ ↑n.
+#m #n elim m -m
+/2 width=1 by nle_succ_bi/
+qed-.