Commit 2020-09-02 13:19 ddbdfeb5

chore(data/fin): succ_above defn compares fin terms instead of values (#3999) fin.succ_above is redefined to use a comparison between two fin (n + 1) instead of their coerced values in nat. This should delay any "escape" from fin into nat until necessary. Lemmas are added regarding fin.succ_above. Some proofs for existing lemmas reworked for new definition and simplified. Additionally, docstrings are added for related lemmas. New lemmas: Comparison after embedding: succ_above_lt_ge succ_above_lt_gt Injectivity lemmas: succ_above_right_inj succ_above_right_injective succ_above_left_inj succ_above_left_injective finset lemma: fin.univ_succ_above prod and sum lemmas: fin.prod_univ_succ_above