Description: Congruence commutes on the LHS. Variant of Theorem 2.5 of Schwabhauser p. 27, but in a convenient form for a common case. (Contributed by David A. Wheeler, 29-Jun-2020)