Commit 2023-10-27 17:23 f52e2714

chore: ofNat lemmas for Complex.normSq and abs (#7975) Having _ofNat lemmas is important for confluence given that for both normSq and abs, the _ofReal lemma is @[simp] and so is ofReal_ofNat. We already have lemmas for 0 and 1 from the bundled classes for both functions, so I'm only adding lemmas for the AtLeastTwo case here.