+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.
+