Commit 2024-05-30 11:03 645bbd3c

chore: deprecate Nat.div_mod_eq_mod_mul_div and Nat.mul_div_mul_comm_of_dvd_dvd (#13336)

• div_mod_eq_mod_mul_div is a flipped version of mod_mul_right_div_self.
• mul_div_mul_comm_of_dvd_dvd is a flipped version of div_mul_div_comm. These were found by tryAtEachStep.