feat(data/fin): cast_succ_mk and other lemmas (#6094)
* add lemmas for all the `fin.cast_*` functions which describe what happens to an "explicitly presented" term of `fin n`, built from the constructor
* fixes some errors in doc-strings
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
