Ring congruence induction compatibility

This file restores the upstream eliminator name used by the Brauer group port.

theorem RingCon.quot_ind {R : Type u_1} [Ring R] (r : RingCon R) {motive : r.Quotient → Prop} (basic : ∀ (x : R), motive (r.mk' x)) (x : r.Quotient) : motive x