huge commit in automation:

[helm.git] / helm / software / matita / library / nat / div_and_mod.ma

diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma
index e31f2d678cd739a075e5e33b5847998157f5d4fc..cbab87206ee5457cf967e25505b3772ed9180b15 100644 (file)
--- a/helm/software/matita/library/nat/div_and_mod.ma
+++ b/helm/software/matita/library/nat/div_and_mod.ma
@@ -147,7 +147,7 @@ apply le_plus_n.
 rewrite < sym_times.
 rewrite > distr_times_minus.
 rewrite > plus_minus.
-lapply(plus_to_minus ??? H3); demodulate. reflexivity.
+lapply(plus_to_minus ??? H3); demodulate all.
 (*
 rewrite > sym_times.
 rewrite < H5.