rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
qed.
variant assoc_Ztimes : \forall x,y,z:Z.
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
qed.
variant assoc_Ztimes : \forall x,y,z:Z.