The snake lemma

Stream: homology

[Joël Riou]

In PR #8081 and #8084 I obtain the snake lemma by using the new API of the homology refactor (thanks again @Johan Commelin for all the PR reviews!). It is based on the use of "refinements" in order to do some diagram chases, the duality so as to reduce the effort by half, and the use of the category of short complexes makes it easier as compared to the LTE.

[Riccardo Brasca]

I've left a couple of cosmetic comments about #8081, but LGTM.