intro.elim p.
absurd (O < n).assumption.apply le_to_not_lt.assumption.
cut ((n1 \divides m) \lor (n1 \ndivides m)).
-change with
-((match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides m \land
-(match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1).
+simplify.
elim Hcut.rewrite > divides_to_divides_b_true.
simplify.
split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
-change with
-(gcd_aux n n1 (m \mod n1) \divides m \land
-gcd_aux n n1 (m \mod n1) \divides n1).
+simplify.
cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
gcd_aux n n1 (m \mod n1) \divides mod m n1).
elim Hcut1.
theorem divides_gcd_nm: \forall n,m.
gcd n m \divides m \land gcd n m \divides n.
intros.
+(*CSC: simplify simplifies too much because of a redex in gcd *)
change with
(match leb n m with
[ true \Rightarrow
d \divides m \to d \divides n \to d \divides gcd_aux p m n.
intro.elim p.
absurd (O < n).assumption.apply le_to_not_lt.assumption.
-change with
-(d \divides
-(match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)])).
+simplify.
cut (n1 \divides m \lor n1 \ndivides m).
elim Hcut.
rewrite > divides_to_divides_b_true.
simplify.assumption.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
-change with (d \divides gcd_aux n n1 (m \mod n1)).
+simplify.
apply H.
cut (O \lt m \mod n1 \lor O = m \mod n1).
elim Hcut1.assumption.
theorem divides_d_gcd: \forall m,n,d.
d \divides m \to d \divides n \to d \divides gcd n m.
intros.
+(*CSC: here simplify simplifies too much because of a redex in gcd *)
change with
(d \divides
match leb n m with
absurd (O < n).assumption.apply le_to_not_lt.assumption.
cut (O < m).
cut (n1 \divides m \lor n1 \ndivides m).
-change with
-(\exists a,b.
-a*n1 - b*m = match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]
-\lor
-b*m - a*n1 = match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]).
+simplify.
elim Hcut1.
rewrite > divides_to_divides_b_true.
simplify.
qed.
theorem symmetric_gcd: symmetric nat gcd.
+(*CSC: bug here: unfold symmetric does not work *)
change with
(\forall n,m:nat. gcd n m = gcd m n).
intros.
theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
gcd n m = (S O).
-intros.unfold prime in H.change with (gcd n m = (S O)).
+intros.unfold prime in H.
elim H.
apply antisym_le.
-apply not_lt_to_le.
-change with ((S (S O)) \le gcd n m \to False).intro.
+apply not_lt_to_le.unfold Not.unfold lt.
+intro.
apply H1.rewrite < (H3 (gcd n m)).
apply divides_gcd_m.
apply divides_gcd_n.assumption.
theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
n \divides p \lor n \divides q.
intros.
-cut (n \divides p \lor n \ndivides p).
-elim Hcut.
-left.assumption.
-right.
-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.
-rewrite > distr_times_minus.
-rewrite > (sym_times q (a1*p)).
-rewrite > (assoc_times a1).
-elim H1.rewrite > H6.
-rewrite < (sym_times n).rewrite < assoc_times.
-rewrite > (sym_times q).rewrite > assoc_times.
-rewrite < (assoc_times a1).rewrite < (sym_times n).
-rewrite > (assoc_times n).
-rewrite < distr_times_minus.
-apply (witness ? ? (q*a-a1*n2)).reflexivity.
-(* second case *)
-rewrite > (times_n_SO q).rewrite < H5.
-rewrite > distr_times_minus.
-rewrite > (sym_times q (a1*p)).
-rewrite > (assoc_times a1).
-elim H1.rewrite > H6.
-rewrite < sym_times.rewrite > assoc_times.
-rewrite < (assoc_times q).
-rewrite < (sym_times n).
-rewrite < distr_times_minus.
-apply (witness ? ? (n2*a1-q*a)).reflexivity.
-(* end second case *)
-rewrite < (prime_to_gcd_SO n p).
-apply eq_minus_gcd.
-assumption.assumption.
-apply (decidable_divides n p).
-apply (trans_lt ? (S O)).unfold lt.apply le_n.
-unfold prime in H.elim H. assumption.
+cut (n \divides p \lor n \ndivides p)
+ [elim Hcut
+ [left.assumption
+ |right.
+ 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.
+ rewrite > distr_times_minus.
+ rewrite > (sym_times q (a1*p)).
+ rewrite > (assoc_times a1).
+ elim H1.rewrite > H6.
+ (* applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
+ reflexivity. *);
+ applyS (witness n ? ? (refl_eq ? ?)).
+ (*
+ rewrite < (sym_times n).rewrite < assoc_times.
+ rewrite > (sym_times q).rewrite > assoc_times.
+ rewrite < (assoc_times a1).rewrite < (sym_times n).
+ rewrite > (assoc_times n).
+ rewrite < distr_times_minus.
+ apply (witness ? ? (q*a-a1*n2)).reflexivity
+ *)
+ |(* second case *)
+ rewrite > (times_n_SO q).rewrite < H5.
+ rewrite > distr_times_minus.
+ rewrite > (sym_times q (a1*p)).
+ rewrite > (assoc_times a1).
+ elim H1.rewrite > H6.
+ rewrite < sym_times.rewrite > assoc_times.
+ rewrite < (assoc_times q).
+ rewrite < (sym_times n).
+ rewrite < distr_times_minus.
+ apply (witness ? ? (n2*a1-q*a)).reflexivity
+ ](* end second case *)
+ |rewrite < (prime_to_gcd_SO n p)
+ [apply eq_minus_gcd|assumption|assumption
+ ]
+ ]
+ ]
+ |apply (decidable_divides n p).
+ apply (trans_lt ? (S O))
+ [unfold lt.apply le_n
+ |unfold prime in H.elim H. assumption
+ ]
+ ]
qed.
theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to