Lemma times_is_distributive : forall n1 n2 n3 : natural,
  times n1 (plus n2 n3) = plus (times n1 n2) (times n1 n3).
Proof.
  intros n1 n2 n3.
  induction n1.

  Case "n1 = zero".
  simpl times.
  reflexivity.

  Case "n1 = succ n1'".
  rewrite times_is_commutative.
  rewrite reverse_times.
  rewrite times_is_commutative.
  rewrite IHn1.
  simpl times.
  assert (H1: (plus (times n1 n2) n2) = (plus n2 (times n1 n2))).
  rewrite plus_is_commutative.
  reflexivity.
  assert (H2: (plus (times n1 n3) n3) = (plus n3 (times n1 n3))). rewrite plus_is_commutative. reflexivity.
  rewrite H1. rewrite H2.
  assert (H3: (plus (plus n2 (times n1 n2)) (plus n3 (times n1 n3)))
    = (plus n2 (plus (times n1 n2) (plus n3 (times n1 n3))))). rewrite plus_is_associative. reflexivity.
  assert (H4: (plus (times n1 n2) (plus n3 (times n1 n3)))
    = (plus (plus (times n1 n2) n3) (times n1 n3))). rewrite plus_is_associative. reflexivity.
  rewrite H3. rewrite H4.
  assert (H5: (plus (times n1 n2) n3) = (plus n3 (times n1 n2))). rewrite plus_is_commutative. reflexivity.
  rewrite H5.
  assert (H6: (plus (plus n3 (times n1 n2)) (times n1 n3)) = plus n3 (plus (times n1 n2) (times n1 n3))).
  rewrite plus_is_associative. reflexivity.
  rewrite H6.
  assert (H7: (plus n2 (plus n3 (plus (times n1 n2) (times n1 n3)))) = (plus (plus n2 n3) (plus (times n1 n2) (times n1 n3)))). rewrite plus_is_associative. reflexivity.
  rewrite H7.
  reflexivity.
Qed.