(*** minus *)
definition nminus: nat → nat → nat ≝
- λm,n. npred^n m.
+ λm,n. (npred^n) m.
interpretation
"minus (non-negative integers)"
// qed.
(*** minus_SO_dx *)
-lemma nminus_one_dx (m): ↓m = m - 𝟏 .
+lemma nminus_unit_dx (m): ↓m = m - 𝟏 .
// qed.
(*** eq_minus_S_pred *)