qed.
theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
-ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*m = (gcd_aux p m n) \lor b*m - a*n = (gcd_aux p m n))).
+\exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
intro.
elim p.
absurd O < n.assumption.apply le_to_not_lt.assumption.
cut O < m.
cut (divides n1 m) \lor \not (divides n1 m).
change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
a*n1 - b*m = match divides_b n1 m with
[ true \Rightarrow n1
| false \Rightarrow gcd_aux n n1 (mod m n1)]
\lor
b*m - a*n1 = match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)])).
+| false \Rightarrow gcd_aux n n1 (mod m n1)].
elim Hcut1.
rewrite > divides_to_divides_b_true.
simplify.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
a*n1 - b*m = gcd_aux n n1 (mod m n1)
\lor
-b*m - a*n1 = gcd_aux n n1 (mod m n1))).
+b*m - a*n1 = gcd_aux n n1 (mod m n1).
cut
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
\lor
-b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1))).
+b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1).
elim Hcut2.elim H5.elim H6.
(* first case *)
rewrite < H7.
apply lt_to_le_to_lt ? n1.assumption.assumption.
qed.
-theorem eq_minus_gcd: \forall m,n.
-ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m))).
+theorem eq_minus_gcd:
+ \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
intros.
change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
a*n - b*m =
match leb n m with
[ true \Rightarrow
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
-)).
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
apply leb_elim n m.
apply nat_case1 n.
simplify.intros.
apply sym_eq.apply minus_n_O.
intros.
change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
-\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)))).
+\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)).
apply eq_minus_gcd_aux.
simplify. apply le_S_S.apply le_O_n.
assumption.apply le_n.
apply sym_eq.apply minus_n_O.
intros.
change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
-\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)))).
+\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)).
cut
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
\lor
-b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))).
+b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)).
elim Hcut.elim H2.elim H3.
apply ex_intro ? ? a1.
apply ex_intro ? ? a.
apply le_to_or_lt_eq.apply le_O_n.
qed.
-(* esempio di sfarfallalmento !!! *)
-(*
-theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to
-divides n p \lor divides n q.
-intros.
-cut divides n p \lor \not (divides n p).
-elim Hcut.left.assumption.
-right.
-cut ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*p = (S O) \lor b*p - a*n = (S O))).
-elim Hcut1.elim H3.*)
-
theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
divides n p \lor divides n q.
intros.
elim Hcut.
left.assumption.
right.
-cut ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*p = (S O) \lor b*p - a*n = (S O))).
+cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
elim Hcut1.elim H3.elim H4.
(* first case *)
rewrite > times_n_SO q.rewrite < H5.