From 0e49deb1c20717b0a479f0bfc871c0732946ec79 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 25 Mar 2010 09:22:23 +0000 Subject: [PATCH] cosi va (se vi pare). From: asperti --- helm/software/matita/nlibrary/arithmetics/R.ma | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) 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. -- 2.39.2