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