qed.
variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def
associative_times.
lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
qed.
variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def
associative_times.
lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).