(ord_rem n (nth_prime (max_prime_factor n))))
[apply lt_to_le.assumption
|apply le_n
- |autobatch
+ |apply sym_eq.
+ apply p_ord_exp1.apply lt_O_nth_prime_n.
+ apply not_divides_ord_rem.apply lt_S_to_lt. apply H.
+ apply lt_SO_nth_prime_n.rewrite > sym_times.rewrite < Hletin.
+ reflexivity.
|assumption
]
|left.apply sym_eq.assumption