(* ARITHMETICAL PROPERTIES **************************************************)
+(* Iota equations ***********************************************************)
+
+lemma pred_O: pred 0 = 0.
+normalize // qed.
+
+lemma pred_S: ∀m. pred (S m) = m.
+// qed.
+
(* Equations ****************************************************************)
+lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
+// qed-.
+
(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
(* Inversion & forward lemmas ***********************************************)
+lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
+// qed-.
+
lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
/2 width=1 by monotonic_pred/ qed-.
lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
/2 width=4 by plus_xySz_x_false/ qed-.
+(* Note this should go in nat.ma *)
+lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+#x @(nat_ind_plus … x) -x /2 width=1 by or_introl/
+#x #_ #y @(nat_ind_plus … y) -y /2 width=1 by or_intror/
+#y #_ >minus_plus_plus_l
+#H lapply (discr_plus_xy_minus_xz … H) -H
+#H destruct
+qed-.
+
+lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y.
+* /2 width=1 by conj/ #x #y normalize #H destruct
+qed-.
+
(* Iterators ****************************************************************)
(* Note: see also: lib/arithemetics/bigops.ma *)
interpretation "iterated function" 'exp op n = (iter n ? op).
+lemma iter_O: ∀B:Type[0]. ∀f:B→B.∀b. f^0 b = b.
+// qed.
+
+lemma iter_S: ∀B:Type[0]. ∀f:B→B.∀b,l. f^(S l) b = f (f^l b).
+// qed.
+
lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b).
#B #f #b #l >commutative_plus //
qed.