auto rewritten with only one tail recursive function.

[helm.git] / matita / library_auto / auto / nat / euler_theorem.ma

diff --git a/matita/library_auto/auto/nat/euler_theorem.ma b/matita/library_auto/auto/nat/euler_theorem.ma
index 8d16ac7234c975a85f0113f661a3c7872217ad60..232ace21fa299d506898a67dc862e08f95f40b36 100644 (file)
--- 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)