+(* Constructions with niter *************************************************)
+
+(*** iter_plus *)
+lemma niter_plus (A) (f) (a) (n1) (n2):
+ f^n1 (f^n2 a) = f^{A}(n1+n2) a.
+#A #f #a #n1 #n2 @(nat_ind_succ โฆ n2) -n2 //
+#n2 #IH <nplus_succ_dx <niter_succ <niter_succ <niter_appl //
+qed.
+
+(* Advanved constructions (semigroup properties) ****************************)
+