X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=6da8e13d02780dd627233655593f7dcedf311e2c;hb=a04ff90485bcb7d800538914d0df76eeb414f6c9;hp=cb29da2f87aa67edaf100a3b2533db05e82e1dde;hpb=ff5d15158c83a1f45d78daf99f22de83aed3eab0;p=helm.git

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index cb29da2f8..6da8e13d0 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -384,6 +384,74 @@ rewrite < H4 in \vdash (? ? %).assumption.
 intros.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
+theorem gcd_n_n: \forall n.gcd n n = n.
+intro.elim n
+  [reflexivity
+  |apply le_to_le_to_eq
+    [apply divides_to_le
+      [apply lt_O_S
+      |apply divides_gcd_n
+      ]
+    |apply divides_to_le
+      [apply lt_O_gcd.apply lt_O_S
+      |apply divides_d_gcd
+        [apply divides_n_n|apply divides_n_n]
+      ]
+    ]
+  ]
+qed.
+
+theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
+O < i.
+intros.
+elim (le_to_or_lt_eq ? ? (le_O_n i))
+  [assumption
+  |absurd ((gcd i n) = (S O))
+    [assumption
+    |rewrite < H2.
+     simplify.
+     unfold.intro.
+     apply (lt_to_not_eq (S O) n H).
+     apply sym_eq.assumption
+    ]
+  ]
+qed.
+
+theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
+i < n.
+intros.
+elim (le_to_or_lt_eq ? ? H1)
+  [assumption
+  |absurd ((gcd i n) = (S O))
+    [assumption
+    |rewrite > H3.
+     rewrite > gcd_n_n.
+     unfold.intro.
+     apply (lt_to_not_eq (S O) n H).
+     apply sym_eq.assumption
+    ]
+  ]
+qed.
+
+theorem  gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
+intro.apply (nat_case n)
+  [intros.reflexivity
+  |intros.
+   apply le_to_le_to_eq
+    [apply divides_to_le
+      [apply lt_O_S|apply divides_gcd_n]
+    |apply divides_to_le
+      [apply lt_O_gcd.rewrite > (times_n_O O).
+       apply lt_times[apply lt_O_S|assumption]
+      |apply divides_d_gcd
+        [apply (witness ? ? m1).reflexivity
+        |apply divides_n_n
+        ]
+      ]
+    ]
+  ]
+qed.
+
 theorem symmetric_gcd: symmetric nat gcd.
 (*CSC: bug here: unfold symmetric does not work *)
 change with 
@@ -440,6 +508,41 @@ qed.
 
 (* for the "converse" of the previous result see the end  of this development *)
 
+theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to 
+(gcd n m) = (S O) \to \lnot (divides n m).
+intros.unfold.intro.
+elim H2.
+generalize in match H1.
+rewrite > H3.
+intro.
+cut (O < n2)
+  [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
+    [cut (gcd n (n*n2) = n)
+      [apply (lt_to_not_eq (S O) n)
+        [assumption|rewrite < H4.assumption]
+      |apply gcd_n_times_nm.assumption
+      ]
+    |apply (trans_lt ? (S O))[apply le_n|assumption]
+    |assumption
+    ]
+  |elim (le_to_or_lt_eq O n2 (le_O_n n2))
+    [assumption
+    |apply False_ind.
+     apply (le_to_not_lt n (S O))
+      [rewrite < H4.
+       apply divides_to_le
+        [rewrite > H4.apply lt_O_S
+        |apply divides_d_gcd
+          [apply (witness ? ? n2).reflexivity
+          |apply divides_n_n
+          ]
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 intro.
 apply antisym_le.apply divides_to_le.unfold lt.apply le_n.