auto rewritten with only one tail recursive function.

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

diff --git a/matita/library_auto/auto/nat/congruence.ma b/matita/library_auto/auto/nat/congruence.ma
index 606fdfcf8a061b3ada38bef52a455a0dbd69ea1a..9683869c1aa171e48e7a90ba8c61716c4f2f1173 100644 (file)
--- a/matita/library_auto/auto/nat/congruence.ma
+++ b/matita/library_auto/auto/nat/congruence.ma
@@ -231,9 +231,10 @@ congruent m m1 p \to congruent (n*m) (n1*m1) p.
 unfold congruent. 
 intros. 
 rewrite > (mod_times n m p H).
-auto.
-(*rewrite > H1.
+rewrite > H1.
 rewrite > H2.
+auto.
+(*
 apply sym_eq.
 apply mod_times.
 assumption.*)