-(* da spostare *)
-lemma 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.
-
-(* da spostare *)
-lemma 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_Pi_P: \forall n,k. O < k \to k \le n \to
-gcd n (Pi_P (\lambda i.eqb (gcd i n) (S O)) k) = (S O).