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
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