feat(data/fin): flesh out API for fin (#3769)
Provide more API for `fin n`. Lemma names chosen to match equivalent lemmas in `nat`. Does not develop docstrings for the lemmas.
New lemmas:
iff lemmas for comparison
`ne_iff_vne`
`eq_mk_iff_coe_eq`
`succ_le_succ_iff`
`succ_lt_succ_iff`
lemmas about explicit numerals
`val_zero'`
`mk_zero`
`mk_one`
`mk_bit0`
`mk_bit1`
`cast_succ_zero`
`succ_zero_eq_one`
`zero_ne_one`
`pred_one`
lemmas about order
`zero_le`
`succ_pos`
`mk_succ_pos`
`one_pos`
`one_lt_succ_succ`
`succ_succ_ne_one`
`pred_mk_succ`
`cast_succ_lt_last`
`cast_succ_lt_succ`
`lt_succ`
`last_pos`
`le_coe_last`
coe lemmas:
`coe_eq_cast_succ`
`coe_succ_eq_succ`
`coe_nat_eq_last`
succ_above API:
`succ_above_below`
`succ_above_zero`
`succ_above_last`
`succ_above_above`
`succ_above_pos`
addition API:
`add_one_pos`
`pred_add_one`
Co-authored by: Yury Kudryashov urkud@ya.ru
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
