(*** inv_eq_minus_O *)
lemma nle_eq_minus_O (m) (n): 𝟎 = m - n → m ≤ n.
-#m #n @(nat_ind_succ_2 … m n) //
+#m #n @(nat_ind_2_succ … m n) //
/3 width=1 by nle_succ_bi/
qed.
#n #_ #IH /2 width=3 by nle_trans/
qed.
+(*** minus_le_trans_sn *)
+lemma nle_minus_sn (o) (m) (n): m ≤ n → m - o ≤ n.
+/2 width=3 by nle_trans/ qed.
+
(* Inversions with nminus ***************************************************)
(*** eq_minus_O *)