distributivity

(in-package "ACL2")

(defthm |(* (+ x y) z)|
  (equal (* (+ x y) z) (+ (* x z) (* y z))))

(defthm |(* x (+ y z))|
  (equal (* x (+ y z)) (+ (* x y) (* x z))))