[ O \Rightarrow (S O)
| (S p) \Rightarrow (times n (exp n p)) ].
-interpretation "natural exponent" 'exp a b = (cic:/matita/library_autobatch/nat/exp/exp.con a b).
+interpretation "natural exponent" 'exp a b = (exp a b).
theorem exp_plus_times : \forall n,p,q:nat.
n \sup (p + q) = (n \sup p) * (n \sup q).