Commit 2020-05-15 07:57 b44fa3ca
View on Github →chore(data/int/basic): mark cast_sub with simp attribute (#2687)
I think the reason this didn't have the simp
attribute already was from the time when sub_eq_add_neg
was a simp
lemma, so it wasn't necessary. I'm adding the simp
attribute back now that sub_eq_add_neg
is not a simp
lemma.