qed.
(*** minus_minus_comm *)
-lemma nminus_comm (o) (m) (n): o - m - n = o - n - m.
-#o #m #n @(nat_ind_succ … n) -n //
+lemma nminus_comm_21 (m) (n1) (n2): m - n1 - n2 = m - n2 - n1.
+#m #n1 #n2 @(nat_ind_succ … n2) -n2 //
qed.
(*** minus_minus_comm3 *)
-lemma nminus_comm_231 (n) (m1) (m2) (m3):
- n-m1-m2-m3 = n-m2-m3-m1.
+lemma nminus_comm_231 (m) (n1) (n2) (n3):
+ m-n1-n2-n3 = m-n2-n3-n1.
// qed.