+
+(*** plus_minus_minus_be *)
+lemma nplus_minus_be_be (m1) (m2) (m3):
+ m1 ≤ m2 → m2 ≤ m3 → (m3 - m2) + (m2 - m1) = m3 - m1.
+#m1 #m2 #m3 #Hm12 #Hm23
+>nminus_assoc // <nminus_minus_dx_refl_sn //
+qed-.
+
+(*** plus_to_minus_2 *)
+lemma nminus_plus_swap (m1) (m2) (n1) (n2):
+ m1 ≤ n1 → m2 ≤ n2 → m2+n1 = m1+n2 → n1-m1 = n2-m2.
+#m1 #m2 #n1 #n2 #H1 #H2 #H
+@nminus_plus_dx <nplus_minus_assoc //
+qed-.