The library grows...

[helm.git] / helm / matita / library / nat / exp.ma

diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
index c0d36377305f9f1878cb16f419f27294ed72358f..6fcd9da0ec646620f36b8546af0d54f1854dad2c 100644 (file)
--- a/helm/matita/library/nat/exp.ma
+++ b/helm/matita/library/nat/exp.ma
@@ -37,7 +37,7 @@ theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)).
 intro.simplify.rewrite < times_n_SO.reflexivity.
 qed.
 
-theorem bad : \forall n,p,q:nat. 
+theorem exp_exp_times : \forall n,p,q:nat. 
 eq nat (exp (exp n p) q) (exp n (times p q)).
 intros.
 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.