(*** plus *)
definition nplus: nat → nat → nat ≝
- λm,n. nsucc^n m.
+ λm,n. (nsucc^n) m.
interpretation
"plus (non-negative integers)"
// qed.
(*** plus_SO_dx *)
-lemma nplus_one_dx (n): ↑n = n + 𝟏.
+lemma nplus_unit_dx (n): ↑n = n + 𝟏.
// qed.
(*** plus_n_Sm *)
(*** iter_plus *)
lemma niter_plus (A) (f) (n1) (n2):
- f^n2 â\88\98 f^n1 â\89\90 f^{A}(n1+n2).
+ f^n2 â\88\98 f^n1 â\8a\9c f^{A}(n1+n2).
#A #f #n1 #n2 @(nat_ind_succ … n2) -n2 //
#n2 #IH <nplus_succ_dx
@exteq_repl
/3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
qed.
-(* Advanved constructions (semigroup properties) ****************************)
+(* Advanced constructions (semigroup properties) ****************************)
(*** plus_S1 *)
lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
#m #n @(niter_appl … nsucc)
qed.
-(*** plus_O_n.con *)
+(*** plus_O_n *)
lemma nplus_zero_sn (m): m = 𝟎 + m.
#m @(nat_ind_succ … m) -m //
qed.
(*** commutative_plus *)
lemma nplus_comm: commutative … nplus.
#m @(nat_ind_succ … m) -m //
-qed-. (**) (* gets in the way with auto *)
+qed-. (* * gets in the way with auto *)
(*** associative_plus *)
lemma nplus_assoc: associative … nplus.
(* Helper constructions *****************************************************)
(*** plus_SO_sn *)
-lemma nplus_one_sn (n): ↑n = 𝟏 + n.
+lemma nplus_unit_sn (n): ↑n = 𝟏 + n.
#n <nplus_comm // qed.
lemma nplus_succ_shift (m) (n): ↑m + n = m + ↑n.