should be `maxe_pMr` #1389

Closed

Labels

renaming/refactoring 🔧

Milestone

opened

on Nov 12, 2024

analysis/reals/constructive_ereal.v

Line 2436 in 7e2988d

Lemma maxeMr z x y : z \is a fin_num -> 0 <= z ->

like maxr_pMr

Metadata

Assignees

No one assigned

Labels

renaming/refactoring 🔧

Type

No type

Projects

No projects

Milestone

1.8.0

Relationships

None yet

Development

No branches or pull requests