From 39b6427bb73ffd7f3149a1efdd73e604f315a058 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 18 Jan 2010 10:34:24 +0000 Subject: [PATCH] // is now more powerful --- .../software/matita/nlibrary/topology/igft3.ma | 18 ++---------------- 1 file changed, 2 insertions(+), 16 deletions(-) diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma index 904a17a9e..e242cb882 100644 --- a/helm/software/matita/nlibrary/topology/igft3.ma +++ b/helm/software/matita/nlibrary/topology/igft3.ma @@ -197,24 +197,10 @@ nqed. | S _ ⇒ S m * skipfact (pred m) * skipfact (pred m) ]] **) -ntheorem psym_plus: ∀n,m. n + m = m + n. - #n; nelim n - [ #m; nelim m; //; #n0; #H; - nchange with (natS n0 = natS (n0 + O)); - nrewrite < H; // - | #n0; #H; #m; nchange with (S (n0 + m) = m + S n0); - nrewrite > (H …); - nelim m; //; - #n1; #E; nrewrite > E; //] +ntheorem psym_plus: ∀n,m. n + m = m + n.//. nqed. -nlemma easy1: ∀n:nat. two * (S n) = two + two * n. - #n; nelim n;//; - #n0; #H; nnormalize; - nrewrite > (psym_plus ??); - nrewrite > H; nnormalize; - nrewrite > (psym_plus ??); - //. +nlemma easy1: ∀n:nat. two * (S n) = two + two * n.//. nqed. ndefinition skipfact_dom: uuAx. -- 2.39.2