-intros.elim x.
-simplify.apply times_n_O.
-simplify.rewrite > H.apply times_n_Sm.
+intros.elim x;
+ [ simplify. apply times_n_O.
+ | demodulate. reflexivity. (*
+(* applyS times_n_Sm. *)
+simplify.rewrite > H.apply times_n_Sm.*)]
qed.
variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
\def distributive_times_plus.
theorem associative_times: associative nat times.
qed.
variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
\def distributive_times_plus.
theorem associative_times: associative nat times.
rewrite > distr_times_plus.
rewrite < sym_times.
rewrite < (sym_times (times n y) z).
rewrite < H.apply refl_eq.
rewrite > distr_times_plus.
rewrite < sym_times.
rewrite < (sym_times (times n y) z).
rewrite < H.apply refl_eq.