+
+(* 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-.