Proving goal having the form $P \lor Q$, is it redundant to separate into two cases?

Question

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.

Answer 1

Any statement in any proof is redundant if you consider it ‘too obvious’.

In this case, maybe you consider it obvious that $P \implies P \lor Q$ (and I wouldn’t blame you). It does follow directly from the definition of $\lor$, but it’s nice to be especially clear when writing a proof and so it doesn’t hurt to add it in. It is certainly true, though, that proving $\neg Q \implies P$ will suffice for most readers.

Answer 2

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.