(* Destructions with npred **************************************************)
lemma nle_inv_pred_sn (m) (n): ↓m ≤ n → m ≤ ↑n.
(* Destructions with npred **************************************************)
lemma nle_inv_pred_sn (m) (n): ↓m ≤ n → m ≤ ↑n.