Commit 2024-11-03 17:58 e8525898

chore(Data/{Nat,Int}/Cast): move nsmul_one/zsmul_one lemmas (#18525) These two lemmas can be proven without the machinery of ring homomorphisms from the natural numbers / integers, although the proof is slightly less conceptual. The goal is to drop an import of Data.Int.Cast.Lemmas in #18520.