Hi everyone. Hope you're having a lovely Saturday. I'm trying to understand the advantage of writing `extremumP`

in this way

```
Context {T : eqType} (ord : rel T) {I : finType} (P : pred I) (F : I -> T).
Variant extremum_spec : I -> Type :=
ExtremumSpec (i : I) of P i & (forall j : I, P j -> ord (F i) (F j)) :
extremum_spec ord P F i.
Lemma extremumP : extremum_spec ord P F extremum.
```

instead of simply

```
Lemma extremumP : forall j : I, ord (F extremum) (F j)
```

or something like that.

(sorry I have only a few seconds) The purpose of "spec" lemmas is to be used with the `case`

tactic. I or someone else will come back later to cite the related section of the mathcomp book.

Thank you @Cyril Cohen :smile:

See section 5.2.1 of the mathcomp book: https://math-comp.github.io/mcb/

Last updated: Jul 15 2024 at 20:02 UTC