#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-.