Totient function and related files.

[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 8cb4867ff28f6f607a487237ed45991e73d9b69e..eb2043c98f27a7f07b18fa54e4c128ab8cfaa33a 100644 (file)
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -432,6 +432,29 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 qed.
 
+theorem divides_gcd_mod: \forall m,n:nat. O < n \to O < m \to
+divides (gcd m n) (gcd n (m \mod n)).
+intros.
+apply divides_d_gcd.
+apply divides_mod.assumption.
+apply divides_gcd_n.
+apply divides_gcd_m.
+apply divides_gcd_m.
+qed.
+
+theorem divides_mod_gcd: \forall m,n:nat. O < n \to O < m \to
+divides (gcd n (m \mod n)) (gcd m n) .
+intros.
+apply divides_d_gcd.
+apply divides_gcd_n.
+apply divides_mod_to_divides ? ? n.
+assumption.
+apply divides_gcd_m.
+apply divides_gcd_n.
+qed.
+
+(* gcd and primes *)
+
 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 gcd n m = (S O).
 intros.simplify in H.change with (gcd n m = (S O)).