I just want to learn how to use Coq better.
Supposing I wanted to prove a statement like “a vector space is naturally isomorphic to its dual”.
I would like to see how to define the concepts used in this statement, and then the statement proven, from scratch, in Coq. I do not wish to use a pre-existing library which has such objects already defined. I would like to see it done from the lowest level possible. I am pretty sure I read that Coq, based on the calculus of inductive constraints, has some sort of “core library”, its absolutemost primitives, vs. a number of concepts and definitions it commonly comes supplied with, like a “standard library”. My wish is to see the definitions constructed from the minimal base; the former instead of the latter.