Add ∣m+n∣n⇒∣m to Data.Nat.Divisiblity

[Taneb]

Also slightly simplify the proof of ∣m+n∣m⇒∣n, which is closely related

[gallais]

Based on the other proof, I presume that this is a typo on the variable name.

Suggested change

	∣m+n∣n⇒∣m {d} {m} {n} (divides p m*n≡p*d) (divides-refl q) =
	divides (p ∸ q) $ begin-equality
	m ≡⟨ m+n∸n≡m m n ⟨
	m + n ∸ n ≡⟨ cong (_∸ q * d) m*n≡p*d ⟩
	p * d ∸ q * d ≡⟨ *-distribʳ-∸ d p q ⟨
	(p ∸ q) * d ∎
	∣m+n∣n⇒∣m {d} {m} {n} (divides p m+n≡p*d) (divides-refl q) =
	divides (p ∸ q) $ begin-equality
	m ≡⟨ m+n∸n≡m m n ⟨
	m + n ∸ n ≡⟨ cong (_∸ q * d) m+n≡p*d ⟩
	p * d ∸ q * d ≡⟨ *-distribʳ-∸ d p q ⟨
	(p ∸ q) * d ∎

Also, why prove it by going back to the core argument instead of invoking ∣m+n∣m⇒∣n and
the fact _+_ is commutative?

[Taneb]

Also, why prove it by going back to the core argument instead of invoking ∣m+n∣m⇒∣n and
the fact _+_ is commutative?

I felt like this new proof is the more natural variant (the other already uses +-comm in its proof) and I don't like using subst if I can help it