Cancellation of a common factor in a congruence (source code)

= Cancellation of a common factor in a congruence
{title2=$ac\equiv bc\pmod n\iff a\equiv b\pmod{n/\gcd(c,n)}$}

For <integers> $a,b$ and positive <integers> $c,n$, a common factor may be cancelled from a <integer congruence> provided the modulus is divided by the corresponding <greatest common divisor>. Let $d=\gcd(c,n)$, $c=dc'$, and $n=dn'$. The <integers> $c',n'$ are coprime: any common divisor greater than one would give a common divisor of $c,n$ larger than $d$.

By <divisibility> and <Euclid's lemma>,
$$
ac\equiv bc\pmod n
\iff n'\mid c'(a-b)
\iff n'\mid a-b.
$$
This proves the displayed equivalence. If $c$ is coprime to $n$, the modulus stays unchanged and this is ordinary cancellation by a <modular multiplicative inverse>. If $n\mid c$, the reduced modulus is $1$, so every pair $a,b$ satisfies the reduced <integer congruence>.