New entry: fermat's little theorem (almost complete).

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

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 520e99ea8f1e7a7d58f0a964fdd9021076b17938..71734fad3a58ff17c619da36325bbd13dca6c415 100644 (file)
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -144,7 +144,6 @@ rewrite > sym_times.
 rewrite < H5.
 rewrite < sym_times.
 apply plus_to_minus.
-apply eq_plus_to_le ? ? ? H3.
 apply H3.
 apply le_times_r.
 apply lt_to_le.
@@ -171,7 +170,6 @@ rewrite > sym_times.
 rewrite < H3.
 rewrite < sym_times.
 apply plus_to_minus.
-apply eq_plus_to_le ? ? ? H5.
 apply H5.
 apply le_times_r.
 apply lt_to_le.