[lotsofpulp]

Is a contrapositive a corollary? P implies Q is logically equivalent to Not Q implies Not P.

A corollary would be some other relation that can be deduced as a result of P implies Q, not simply a restatement of P implies Q.

(Using the discrete math definition of imply, not the colloquial definition of imply).

[moefh]

Yes, a corollary can be just the contrapositive of something you just proved. Sometimes it's even more trivial, like a special case of a general theorem you proved.

A very common use is to re-state something so it's in the exact form of something you said you'd prove. Another common case is to highlight a nice incidental result that's a bit outside the path towards the main result -- for example, it immediately follows (perhaps logically equivalent to) something that's been proven, but it's dressed in a way that catches the attention of someone who's just skimming.