+(*
+theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H5 in H4.
+elim (divides_times_to_divides ? ? ? H1 H4)
+ [elim H.apply False_ind.
+ apply H2.apply sym_eq.apply H8
+ [assumption
+ |apply prime_to_lt_SO.assumption
+ ]
+ |elim H6.
+ apply (witness ? ? n1).
+ rewrite > assoc_times.
+ rewrite < H7.assumption
+ ]
+qed.
+*)
+
+theorem divides_to_divides_times: \forall p,q,n. prime p \to p \ndivides q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H4 in H2.
+elim (divides_times_to_divides ? ? ? H H2)
+ [apply False_ind.apply H1.assumption
+ |elim H5.
+ autobatch by transitive_divides, H5, reflexive_divides,divides_times.
+ (*
+ apply (witness ? ? n2).
+ rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+ rewrite > assoc_times.
+ autobatch.
+ (*rewrite < H6.assumption*)
+ *)
+ ]
+qed.
\ No newline at end of file