theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
=defactorize_aux g m*defactorize_aux h m.
intro.elim g
- [elim h;simplify;autobatch
+ [elim h;simplify;autobatch;
|elim h
[simplify;autobatch
|simplify.rewrite > (H n3 (S m)).autobatch