(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/exp".
-
include "nat/div_and_mod.ma".
include "nat/lt_arith.ma".
[ O \Rightarrow (S O)
| (S p) \Rightarrow (times n (exp n p)) ].
-interpretation "natural exponent" 'exp a b = (cic:/matita/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).