X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fgcd.ma;fp=matita%2Fmatita%2Flib%2Farithmetics%2Fgcd.ma;h=1490a626e336db7cc42c65f804e9e3b66b15e078;hb=31e8729021717072f88d250ef41527da3488289e;hp=104b598626cd73e3dc3d43c56c5eed86e3fed2ae;hpb=83a494ff9e15871231c8338df95f89926f2293ba;p=helm.git

diff --git a/matita/matita/lib/arithmetics/gcd.ma b/matita/matita/lib/arithmetics/gcd.ma
index 104b59862..1490a626e 100644
--- a/matita/matita/lib/arithmetics/gcd.ma
+++ b/matita/matita/lib/arithmetics/gcd.ma
@@ -54,7 +54,7 @@ qed.
 
 lemma divides_to_gcd_aux: ∀p,m,n. O < p → O < n →n ∣ m → 
   gcd_aux p m n = n.
-#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm normalize 
+#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm whd in ⊢ (??%?)
 >divides_to_dividesb_true normalize //
 qed.
 
@@ -69,7 +69,7 @@ qed.
 
 lemma not_divides_to_gcd_aux: ∀p,m,n. 0 < n → n ∤ m → 
   gcd_aux (S p) m n = gcd_aux p n (m \mod n).
-#p #m #n #lenm #divnm normalize >not_divides_to_dividesb_false
+#p #m #n #lenm #divnm whd in ⊢ (??%?) >not_divides_to_dividesb_false
 normalize // qed.
 
 theorem divides_gcd_aux_mn: ∀p,m,n. O < n → n ≤ m → n ≤ p →