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

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

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 36c7a96597fef1f5b83169d5b08af8c842ba30b4..eb1053feb78cb5e88a70a9154ff9af271f15e08b 100644 (file)
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -46,13 +46,9 @@ rewrite < assoc_times.
 rewrite < H4.
 apply sym_eq.
 apply plus_to_minus.
-rewrite > div_mod m n in \vdash (? ? %).
 rewrite > sym_times.
-apply eq_plus_to_le ? ? (m \mod n).
-reflexivity.
+apply div_mod.
 assumption.
-rewrite > sym_times.
-apply div_mod.assumption.
 qed.
 
 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to