+(* Destructions with npred **************************************************)
+
+lemma nle_inv_pred_sn (m) (n): ↓m ≤ n → m ≤ ↑n.
+#m #n @(nat_ind_succ … m) -m
+/2 width=1 by nle_succ_bi/
+qed-.
+
+(* Constructions with npred *************************************************)
+
+lemma nle_succ_pred_dx_refl (m): m ≤ ↑↓m.
+#m @nle_inv_pred_sn // qed.