X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fdiv_and_mod.ma;h=cbab87206ee5457cf967e25505b3772ed9180b15;hb=73a66cce6e72c654fdcd0ce760c405a74af70d08;hp=e31f2d678cd739a075e5e33b5847998157f5d4fc;hpb=5c10d402b5de7233bc83d7f685b274832e383212;p=helm.git

diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma
index e31f2d678..cbab87206 100644
--- 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.