mathlib

21e9d424 - feat(algebra/euclidean_domain): Unify occurences of div_add_mod and mod_add_div (#5884)

feat(algebra/euclidean_domain): Unify occurences of div_add_mod and mod_add_div (#5884) Adding the corresponding commutative version at several places (euclidean domain, nat, pnat, int) whenever there is the other version. In subsequent PRs other proofs in the library which now use some version of `add_comm, exact div_add_mod` or `add_comm, exact mod_add_div` should be golfed. Trying to address issue #1534 Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>