check removed

[helm.git] / matita / matita / lib / tutorial / chapter2.ma

diff --git a/matita/matita/lib/tutorial/chapter2.ma b/matita/matita/lib/tutorial/chapter2.ma
index 7dda6e6f2c9bc2f06d55d530cf95de96465a6df8..1f0244505e3d54333a795f27f16da66ed5686507 100644 (file)
--- a/matita/matita/lib/tutorial/chapter2.ma
+++ b/matita/matita/lib/tutorial/chapter2.ma
@@ -26,7 +26,7 @@ ones you received in input. Most mathematical functions can be naturally defined
 in this way. For instance, the sum of two natural numbers can be defined as 
 follows: *)
 
-let rec add n m ≝ 
+let rec add n (m:nat) ≝ 
 match n with
 [ O ⇒ m
 | S a ⇒ S (add a m)
@@ -373,3 +373,20 @@ normalize // qed.
 example quotient8: witness … (div2Pagain (twice (twice (twice (twice (S O)))))) 
        = 〈twice (twice (twice (S O))), ff〉.
 // qed. 
+
+(********************)
+
+inductive Pari : nat → Prop ≝
+   | pariO : Pari O
+   | pari2 : ∀x. Pari x → Pari (S (S x)).
+   
+definition natPari ≝ Sub nat Pari.
+
+definition addPari: natPari → natPari → natPari.
+* #a #Ha * #b #Hb @(mk_Sub … (add a b))  
+elim Ha
+  [normalize @Hb
+  |#x #Hx #Hind normalize @pari2 @Hind
+  ]
+qed.    
+