I am trying to port a repo to mathcomp 2.1, while I found that the definition `bigmaxr`

is deprecated. It is suggested by mathcomp 2.1 to "Use topology.v's bigmax/min lemmas instead". However, there aren't many relevant lemmas in the `bigmax/min`

section in file `topology.v`

. Actually I only found four lemmas that "reflects" the boolean and prop definitions.

Can anyone point me to the lemmas that corresponds to those lemma like `bigmaxrP`

that were present in previous versions of mathcomp? Any suggestion or insight will be greatly appreciated!

I am not sure (and cannot check right now) but maybe this is due to an old comment that redirects you to topology.v. The lemmas about bigmax/bigmin that used to live there have been generalized and moved to ssreflect/order.v in the meantime.

Thank you so much! I found the lemmas that I'm using. Your suggestion is really helpful!

Last updated: Jul 15 2024 at 20:02 UTC