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 36fec015971743d1a78e5ae7bda2b9e208f7c0a6..6d936036294637125c97d9253896d9ecc74c5967 100644 (file)
--- 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.