Commit 2020-04-28 15:02 f6c93723

feat(data/fin): add some lemmas about coercions (#2522) Two of these lemmas allow norm_cast to work with inequalities involving fin values converted to ℕ. The rest are for simplifying expressions where coercions are used to convert from ℕ to fin, in cases where an inequality means those coercions do not in fact change the value. There are very few lemmas relating to coercions from ℕ to fin in mathlib at present; the lemma of_nat_eq_coe (and val_add on which it depends, and a few similarly trivial lemmas alongside val_add) is moved from data.zmod.basic to fin.basic for use in proving the other lemmas, while the nat lemma add_mod is moved to data.nat.basic for use in the proof of of_nat_eq_coe, and mul_mod is moved alongside it as suggested in review. These lemmas were found useful in formalising solutions to an olympiad problem, see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations, and seem more generally relevant than to just that particular problem.