Release 0.5.9.

[helm.git] / helm / software / matita / contribs / ng_assembly / common / nat_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma
index 06ace91b2581313105126405c4ea51603ffbccaf..64eeb50f122f07b427be0003725cd2c1b136a6a9 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -35,7 +35,6 @@ nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
  napply refl_eq.
 nqed.
 
-(* !!! da togliere *)
 nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
  #n; #H;
  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
@@ -44,7 +43,6 @@ nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
  napply I.
 nqed.
 
-(* !!! da togliere *)
 nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
  #n; #H;
  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
@@ -60,12 +58,12 @@ nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
           nelim n2;
           nnormalize;
           ##[ ##1: #H; napply refl_eq
-          ##| ##2: #n3; #H; #H1; ndestruct (*nelim (nat_destruct_0_S ? H1)*)
+          ##| ##2: #n3; #H; #H1; nelim (nat_destruct_0_S ? H1)
           ##]
  ##| ##2: #n2; #H; #n3; #H1;
           ncases n3 in H1:(%) ⊢ %;
           nnormalize;
-          ##[ ##1: #H1; ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
+          ##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1)
           ##| ##2: #n4; #H1;
                    napply (H n4 (nat_destruct_S_S … H1))
           ##]
@@ -87,12 +85,12 @@ nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
           nelim n2;
           nnormalize;
           ##[ ##1: #H; napply refl_eq
-          ##| ##2: #n3; #H; #H1; ndestruct (*napply (bool_destruct … (O = S n3) H1)*)
+          ##| ##2: #n3; #H; #H1; napply (bool_destruct … (O = S n3) H1) 
           ##]
  ##| ##2: #n2; #H; #n3; #H1;
           ncases n3 in H1:(%) ⊢ %;
           nnormalize;
-          ##[ ##1: #H1; ndestruct (*napply (bool_destruct … (S n2 = O) H1)*)
+          ##[ ##1: #H1; napply (bool_destruct … (S n2 = O) H1)
           ##| ##2: #n4; #H1;
                    nrewrite > (H n4 H1);
                    napply refl_eq