\def distributive_times_plus.
theorem associative_times: associative nat times.
simplify.intros.
elim x.simplify.apply refl_eq.
simplify.rewrite < sym_times.
\def distributive_times_plus.
theorem associative_times: associative nat times.
simplify.intros.
elim x.simplify.apply refl_eq.
simplify.rewrite < sym_times.