(* *)
(**************************************************************************)
-include "ground/notation/functions/two_0.ma".
+include "ground/arith/pnat_two.ma".
include "ground/arith/nat_le_minus_plus.ma".
include "ground/arith/nat_lt.ma".
(* ARITHMETICAL PROPERTIES FOR λδ-2A ****************************************)
-interpretation
- "zero (non-negative integers)"
- 'Two = (ninj (psucc punit)).
-
(* Equalities ***************************************************************)
lemma plus_n_2: ∀n. (n + 𝟐) = n + 𝟏 + 𝟏.
// qed.
lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >nminus_comm <nminus_assoc_comm_23 //
+#a #b #c1 #H >nminus_comm_21 <nminus_assoc_comm_23 //
qed-.
lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
(* Iterators ****************************************************************)
-lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+𝟏) b = f (f^l b).
+lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. (f^(l+𝟏)) b = f ((f^l) b).
#B #f #b #l
<niter_succ //
qed.