highlight Guarded command (since Coq 8.16)

[yaitskov]

Command: Guarded
Some tactics (e.g. refine) allow to build proofs using fixpoint or cofixpoint constructions. Due to the incremental
nature of proof construction, the check of the termination (or guardedness) of the recursive calls in the fixpoint or
cofixpoint constructions is postponed to the time of the completion of the proof.
The command Guarded allows checking if the guard condition for fixpoint and cofixpoint is violated at some
time of the construction of the proof without having to wait the completion of the proof.

[erikmd]

LGTM, thanks @yaitskov!