Fix: ambiguity with newly introduced divisibility symbol

[MatteoGaetzner]

In newer lean versions, the divisibility symbol $\mid$ (\mid) is already defined, hence

infix:50 " ∣ " => divides

example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) :=
  calc
    x ∣ y   := h₁
    _ = z   := h₂
    _ ∣ 2*z := divides_mul ..

results in an ambiguity. So I replaced this symbol with double pipe $|$ (\|) and updated the explanation as to why we use this symbol instead of the canonical divisibility symbol.

[MichaelJFishman]

Thanks! I also ran into this. Your code change fixed it for me.