But does this do anything meaningful, or is it just pointless drudgery because Coq is a machine and can't 'understand'/assume even simple maths/logic if it isn't explicitly stated? This is not a slight on Coq by any means, just pointing out the difference between human proofs and machine proofs. (Humans can of course be tricked into thinking that subtly false statements are trivially true, which the much more meticulous machine proof would discover)

That is, what is being gained by looking at the vacuously true cases where n<2, when the only interesting base case is the one where the LHS of the implication is true?