Wochoice

[Tragicus]

Motivation for this change

Adds a proof of Zorn's lemma, Hausdorff maximal principle and the well ordering principle.
Contains a patch of contra that we may want to extract.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Contains a patch of contra that we may want to extract.

Do you mean that it ought to be a different PR? (That may help the review process.)

[Tragicus]

I would not go so far as "ought to", the fix is quite trivial, but if you would prefer a different PR, I can do it.

[affeldt-aist]

the fix is quite trivial

Ok. Since there is a number of definitions that are added to contra.v and many canonicals, it didn't look trivial to me ^_^.

if you would prefer a different PR, I can do it.

I think that it is better (different concerns, two commits are maybe better also for the git log).

[CohenCyril]

@Tragicus could you rephrase your commit message so as to make

Co-Authored-By: Georges Gonthier <[email protected]>

a single line separated from the title by a white line, and verbatim (otherwise github does not pick it up)

[proux01]

Argh, I accidentally merged this instead of #1183 and I don't have push right on master to revert that, could someone do it, maybe @CohenCyril ?

[proux01]

Done with @affeldt-aist
@Tragicus could you please reopen the PR, sorry again.

[Tragicus]

Can I also rebase and clean up now?

[proux01]

Sure, thanks

[Tragicus]

Reopened at #1198