(*** minus *)
definition nminus: nat → nat → nat ≝
- λm,n. npred^n m.
+ λm,n. (npred^n) m.
interpretation
- "minus (positive integers)"
+ "minus (non-negative integers)"
'minus m n = (nminus m n).
(* Basic constructions ******************************************************)
// qed.
(*** minus_SO_dx *)
-lemma nminus_one_dx (m): ↓m = m - 𝟏 .
+lemma nminus_unit_dx (m): ↓m = m - 𝟏 .
// qed.
(*** eq_minus_S_pred *)
qed.
(*** minus_minus_comm *)
-lemma nminus_minus_comm (o) (m) (n): o - m - n = o - n - m.
+lemma nminus_comm (o) (m) (n): o - m - n = o - n - m.
#o #m #n @(nat_ind_succ … n) -n //
-qed-.
+qed.
+
+(*** minus_minus_comm3 *)
+lemma nminus_comm_231 (n) (m1) (m2) (m3):
+ n-m1-m2-m3 = n-m2-m3-m1.
+// qed.