feat(algebra/euclidean_domain): Unify occurences of div_add_mod and m…

…od_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>

src/algebra/euclidean_domain.lean

@@ -47,6 +47,9 @@ instance : has_mod R := ⟨euclidean_domain.remainder⟩
 theorem div_add_mod (a b : R) : b * (a / b) + a % b = a :=
 euclidean_domain.quotient_mul_add_remainder_eq _ _
 
+lemma mod_add_div (a b : R) : a % b + b * (a / b) = a :=
+(add_comm _ _).trans (div_add_mod _ _)
+
 lemma mod_eq_sub_mul_div {R : Type*} [euclidean_domain R] (a b : R) :
   a % b = a - b * (a / b) :=
 calc a % b = b * (a / b) + a % b - b * (a / b) : (add_sub_cancel' _ _).symm

src/data/int/basic.lean

@@ -476,6 +476,9 @@ theorem mod_add_div : ∀ (a b : ℤ), a % b + b * (a / b) = a
 | -[1+ m] (n+1:ℕ) := mod_add_div_aux m n.succ
 | -[1+ m] -[1+ n] := mod_add_div_aux m n.succ
 
+theorem div_add_mod (a b : ℤ) : b * (a / b) + a % b = a :=
+(add_comm _ _).trans (mod_add_div _ _)
+
 theorem mod_def (a b : ℤ) : a % b = a - b * (a / b) :=
 eq_sub_of_add_eq (mod_add_div _ _)
 

src/data/pnat/basic.lean

@@ -279,16 +279,19 @@ def mod (m k : ℕ+) : ℕ+ := (mod_div m k).1
 -/
 def div (m k : ℕ+) : ℕ  := (mod_div m k).2
 
-theorem mod_add_div (m k : ℕ+) : (m : ℕ) = (mod m k) + k * (div m k) :=
+theorem mod_add_div (m k : ℕ+) : ((mod m k) + k * (div m k) : ℕ) = m :=
 begin
   let h₀ := nat.mod_add_div (m : ℕ) (k : ℕ),
   have : ¬ ((m : ℕ) % (k : ℕ) = 0 ∧ (m : ℕ) / (k : ℕ) = 0),
   by { rintro ⟨hr, hq⟩, rw [hr, hq, mul_zero, zero_add] at h₀,
        exact (m.ne_zero h₀.symm).elim },
   have := mod_div_aux_spec k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ)) this,
-  exact (this.trans h₀).symm,
+  exact (this.trans h₀),
 end
 
+theorem div_add_mod (m k : ℕ+) : (k * (div m k) + mod m k : ℕ) = m :=
+(add_comm _ _).trans (mod_add_div _ _)
+
 theorem mod_coe (m k : ℕ+) :
  ((mod m k) : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) (k : ℕ) ((m : ℕ) % (k : ℕ)) :=
 begin
@@ -351,7 +354,7 @@ theorem mul_div_exact {m k : ℕ+} (h : k ∣ m) : k * (div_exact m k) = m :=
 begin
  apply eq, rw [mul_coe],
  change (k : ℕ) * (div m k).succ = m,
- rw [mod_add_div m k, dvd_iff'.mp h, nat.mul_succ, add_comm],
+ rw [← mod_add_div m k, dvd_iff'.mp h, nat.mul_succ, add_comm],
 end
 
 theorem dvd_antisymm {m n : ℕ+} : m ∣ n → n ∣ m → m = n :=