X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Flibrary_auto%2Fauto%2Fnat%2Feuler_theorem.ma;h=232ace21fa299d506898a67dc862e08f95f40b36;hb=a1c4c601850c71e094a4703af00f02ca2026d8ed;hp=8d16ac7234c975a85f0113f661a3c7872217ad60;hpb=1b839e0367f89503398442b7990fb6b6d1fa2152;p=helm.git

diff --git a/matita/library_auto/auto/nat/euler_theorem.ma b/matita/library_auto/auto/nat/euler_theorem.ma
index 8d16ac723..232ace21f 100644
--- a/matita/library_auto/auto/nat/euler_theorem.ma
+++ b/matita/library_auto/auto/nat/euler_theorem.ma
@@ -181,7 +181,7 @@ split
       apply (trans_le ? (j -i))
       [ apply divides_to_le
         [(*fattorizzare*)
-          auto (*qui auto e' efficace, ma impiega un tempo piuttosto alto a chiudere il goal corrente*)
+          unfold lt.auto.
           (*apply (lt_plus_to_lt_l i).
           simplify.
           rewrite < (plus_minus_m_m)
@@ -214,7 +214,7 @@ split
       apply (trans_le ? (i -j))
       [ apply divides_to_le
         [(*fattorizzare*)
-          auto (*qui auto e' efficace, ma impiega un tempo piuttosto alto per concludere il goal attuale*)
+          unfold lt.auto.
           (*apply (lt_plus_to_lt_l j).
           simplify.
           rewrite < (plus_minus_m_m)