add a version of Zorn relativized over a given point

[t6s]

Motivation for this change

As a user of Zorn, I sometimes want to have a maximal element over a specified point in the target poset. This PR adds that variation of the lemma.

Things done/to do

• [*] added corresponding entries in CHANGELOG_UNRELEASED.md

• [*] added corresponding documentation in the headers

Compatibility with MathComp 2.0

• [x] I added the label TODO: HB port to make sure someone ports this PR to the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.