-apply (transitive_divides ? n).
-apply divides_max_prime_factor_n.
-assumption.assumption.
-apply divides_b_true_to_divides.
-apply lt_O_nth_prime_n.
-apply divides_to_divides_b_true.
-apply lt_O_nth_prime_n.
-apply divides_max_prime_factor_n.
-assumption.
+autobatch.
+autobatch.
+(*
+ [ apply (transitive_divides ? n);
+ [ apply divides_max_prime_factor_n.
+ assumption.
+ | assumption.
+ ]
+ | apply divides_b_true_to_divides;
+ [ apply lt_O_nth_prime_n.
+ | apply divides_to_divides_b_true;
+ [ apply lt_O_nth_prime_n.
+ | apply divides_max_prime_factor_n.
+ assumption.
+ ]
+ ]
+ ]
+*)
+qed.
+
+theorem divides_to_max_prime_factor1 : \forall n,m. O < n \to O < m \to n \divides m \to
+max_prime_factor n \le max_prime_factor m.
+intros 3.
+elim (le_to_or_lt_eq ? ? H)
+ [apply divides_to_max_prime_factor
+ [assumption|assumption|assumption]
+ |rewrite < H1.
+ simplify.apply le_O_n.
+ ]