-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.
+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 ? ?)) (* timeout=50 *).
+ (*
+ 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 divides_exp_to_divides:
+\forall p,n,m:nat. prime p \to
+p \divides n \sup m \to p \divides n.
+intros 3.elim m.simplify in H1.
+apply (transitive_divides p (S O)).assumption.
+apply divides_SO_n.
+cut (p \divides n \lor p \divides n \sup n1).
+elim Hcut.assumption.
+apply H.assumption.assumption.
+apply divides_times_to_divides.assumption.
+exact H2.
+qed.
+
+theorem divides_exp_to_eq:
+\forall p,q,m:nat. prime p \to prime q \to
+p \divides q \sup m \to p = q.
+intros.
+unfold prime in H1.
+elim H1.apply H4.
+apply (divides_exp_to_divides p q m).