// 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
(* 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.