+
+lemma nle_pred_sn (m) (n): m ≤ ↑n → ↓m ≤ n.
+#m #n @(nat_ind_succ … m) -m //
+/2 width=1 by nle_pred_bi/
+qed-.
+
+(* Inversions with npred ****************************************************)
+
+(*** le_inv_S1 *)
+lemma nle_inv_succ_sn (m) (n):
+ ↑m ≤ n → ∧∧ m ≤ ↓n & n = ↑↓n.
+#m #n * -n
+[ /2 width=3 by nle_refl, conj/
+| #n #Hn /3 width=1 by nle_des_succ_sn, conj/
+]
+qed-.