Commit 2020-08-26 20:24 c1478948

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