From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 25 Mar 2010 09:22:23 +0000 (+0000)
Subject: cosi va (se vi pare).
X-Git-Tag: make_still_working~2961
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e49deb1c20717b0a479f0bfc871c0732946ec79;p=helm.git

cosi va (se vi pare).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>
---

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 36fec0159..6d9360362 100644
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -27,6 +27,12 @@ naxiom Qtimes_distr: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
 naxiom Qmult_one: ∀q:Q. 1 * q = q.
 naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2.
 
+(* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
+
+ntheorem lem1: ∀n:nat.∀q:Q. (n * q + q) = (S n) * q.
+#n; #q; ncut (plus n 1 = S n);##[//##]
+//; nqed.
+
 (*ndefinition aaa ≝ Qtimes_distr.
 ndefinition bbb ≝ Qmult_one.
 ndefinition ccc ≝ Qdivides_mult.*)
@@ -42,12 +48,8 @@ ndefinition R ≝ ∃l,u:Q. locate l u.
 nlet corec Q_to_locate q : locate q q ≝ L q q ?.
  ncut (locate q q = locate q ((2*q+q)/3))
   [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
-  | napply eq_f;
-    ncut ((2 * q + q) = ((2 * q + 1 * q))); //; #H;    
-    ncut (q = ((2 * q + q) / 3)); //;
-    ncut (2 * q + 1 * q = 3 * q); //;
-    /4/ (*CSC: basta applicare la distributivita' a meno di riduzione, altro
-               che 4!*) ]
+  | //;
+  ##]
 nqed.
 
 ndefinition Q_to_R : Q → R.