Commit 2021-01-27 08:41 21e9d424

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