Proving goal having the form $P \lor Q$, is it redundant to separate into two cases? In Velleman's How to Prove It, the strategy given for proving goal of the form $P \lor Q$ goes like this:

If $P$ is true, then clearly $P \lor Q$ is true. Now suppose $P$ is false.
[Proof of Q goes here]
Thus, $P \lor Q$ is true.

I feel like the first sentence is redundant. After all, when proving $P \lor Q$, it's equivalent to proving $\lnot P \to Q$, thus we only need to suppose $\lnot P$ to begin with. 

I think that those are two different ways of proving the same thing. If we want to prove that P or Q is true, we can prove that P is true, or we can prove that Q is true. We could also assume P is false and show that it implies Q is true. Then we would have proven the disjunction as it is logically equivalent to the implication.
