Theorem mult_plus_one : forall n m : nat,
        m * (S n) = m + m * n.
Proof.
        intros m n.
        induction n as [| n'].
        simpl.
        reflexivity.
        simpl.
        rewrite -> IHn'.
        rewrite -> plus_swap.
        reflexivity.
Qed.