From 31d160587c8d15e87959999025713395840c0b26 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 18 Jan 2010 10:39:40 +0000 Subject: [PATCH] // is now more powerful --- .../matita/nlibrary/topology/igft2.ma | 22 ++++--------------- 1 file changed, 4 insertions(+), 18 deletions(-) diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma index 4529b40d5..4ca6460d2 100644 --- a/helm/software/matita/nlibrary/topology/igft2.ma +++ b/helm/software/matita/nlibrary/topology/igft2.ma @@ -135,24 +135,10 @@ nqed. | S m ⇒ S 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. @@ -172,8 +158,8 @@ ntheorem skipfact_partial: | #m; #H; @2 [ nnormalize; @1 | nnormalize; #y; nchange in ⊢ (% → ?) with (y = pred (pred (two * (natone + m)))); - nrewrite > (easy1 …); nchange in ⊢ (% → ?) with (y = two * m); - #E; nrewrite > E; nassumption ]##] + nnormalize; nrewrite < (plus_n_Sm …); nnormalize; + #E; nrewrite > E; napply H ]##] nqed. ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat. -- 2.39.2