New version of the library. nth_prime, gcd, log.

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

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index df045daa732e5310d93245c2164610c74d350ae8..c85bb25c2c04faf4ace9c21e65527f89d6536331 100644 (file)
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -74,6 +74,14 @@ P O \to  (\forall m:nat. P (S m)) \to P n.
 intros.elim n.assumption.apply H1.
 qed.
 
+theorem nat_case1:
+\forall n:nat.\forall P:nat \to Prop. 
+(n=O \to P O) \to  (\forall m:nat. (n=(S m) \to P (S m))) \to P n.
+intros 2.elim n.
+apply H.reflexivity.
+apply H2.reflexivity.
+qed.
+
 theorem nat_elim2 :
 \forall R:nat \to nat \to Prop.
 (\forall n:nat. R O n) \to