Wanted: a "Coq for the working mathematician" Sorry for a possibly off-topic question -- there are four StackExchange subs each of which could be construed as the proper place for this question, and I've just picked the one I'm most familiar with.
I'm trying to obtain a working knowledge of the Coq programming language sufficient to be able to encode and (have it) verify constructive proofs in combinatorics and abstract algebra. The proofs, or at least a portion of them high enough to make me happy, are not really probing the boundaries of constructive mathematics; they require no univalence, no coinduction, and probably not even the full strength of inductive types other than $\mathbb N$ (think Peano arithmetic).
Obviously my first idea was to scour the internet for tutorials, but I found the kind of introduction that I want to be surprisingly scarce if not unavailable. So I'm wondering if someone knows such a source or one is currently being written (if so, how can one contribute?). Here is an outline of what I am looking for:


*

*The focus should be on using Coq for verifying proofs in constructive mathematics, or in even more conservative subsets of it. It should not be on playing around with additional axioms (univalence, classical logic) or other systems (temporal logic etc.); nor should it be on practical software verification. It also shouldn't be a logics textbook with Coq used as illustration for the concepts. I'm abstractly interested in each of the things just mentioned, but what I really am looking for is a tutorial written for mathematicians in general rather than for logicians or HoTTists.

*It should provide hands-on examples of proofs which aren't totally toylike or artificial. (I imagine things like "the conjugate of the conjugate of a partition is the old partition" or "if you sort each row of a matrix in increasing order and then do the same with each columns, then the rows are still increasing" or "$-1$ is a quadratic residue modulo the odd prime $p$ iff $p \equiv 1 \mod 4$".)

*Ideally it should give some guidance on how to set up a Coq project (i. e., more than one .v file) and how to write literate Coq/TeX.

*The text should provide the reader with a survival kit of syntax and basic tactics as early on as possible that theoretically allows formalizing any constructive proof in elementary combinatorics and number theory with enough patience. It should then go on with more advanced tactics that make this less of a pain, possibly even those from ssreflect (if that package is sufficiently stable).
The texts I'm currently trying to follow are Coq'Art and Software Foundations, but it seems they don't really fit the above description very much (and the only English version of Coq'Art is from 2004, which isn't very recent in computer science reckoning).
EDIT: Slightly off-topic, I'm also wondering what it would take to release Coq bundled with its most important user-made contributions like ssreflect, making the learning curve at least a little bit less steep by removing the PITA of compiling an ocaml ecosystem from source...
EDIT 2: Florent Hivert's Coq-Combi project seems to be the thing I was trying to build, and I suspect that reading its sources will be a good step towards learning Coq at least for me. On the other hand, Pierre-Yves Strub offers a bundle with Coq and SSReflect for Windows, which solves another problem I was having (the caveat being that the versions are not the newest). It looks like Coq is becoming usable :)
EDIT3: I feel that, with the progress done by now (particularly by Florent Hivert and others on Coq-Combi), I could learn Coq and get sufficiently experienced in it within half a year of not having to worry about publications, teaching and pretending to keep track of current developments. I am wondering if this is mainly me, or everyone in combinatorics is a half-year away from being able to teach their work to their computer. Meanwhile, I would like to share a talk by Neil Strickland I have just discovered, which is a far better rant about the current state of affairs than I could ever write.
 A: This online book by Adam Chlipala hasn't been mentioned:
Certified Programming with Dependent Types
The reason I suggest it is because of this claim by the author in the introduction:
"Most of the insights for Coq are barely even disseminated among the experts, let alone set down in a tutorial form. I hope to use this book to go a long way towards remedying that."
So not a book aimed at mathematicians but hopefully helpful for getting started nonetheless.
A: A relatively new project, Lean, has created a lot of activity lately, see Lean and Mathlib
with its lots of learning material, driven in part by successful attempts by Kevin Buzzard to teach
Lean to maths undergraduates.
A: My attempt to do something like this for Agda is here: http://neil-strickland.staff.shef.ac.uk/formal/.  I would also like to see a Coq equivalent (also Isabelle, Mizar etc) but I do not currently have the knowledge to write one myself.
A: I might suggest the book devised for the library on GitHub, Mathematical Components (the author of the question is acknowledged within actually). It makes no assumptions on the reader in terms of programming experience. There are of course I imagine an abundance of publications that developed these tools, so I was ecstatic myself to find no specialized background intended for the book's readers. It is written in English and is geared toward the project to formalize mathematics on GitHub, and you'll find in the introduction that in more ways than typical treatments of Coq that are for beginners a bent which is toward mathematical progress being achieved with Coq. Would love to hear reviews for the text in the comments to this answer. I myself just started.
