Helpers for working with star operators on quotients.

TODO: consider defining Star versions of RingCon.

theorem RingConGen.Rel.star {R : Type u_1} [NonUnitalNonAssocSemiring R] [StarRing R] {r : R → R → Prop} (hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)) ⦃a b : R⦄ : Rel r a b → Rel r (Star.star a) (Star.star b)

theorem ringConGen_star {R : Type u_1} [NonUnitalNonAssocSemiring R] [StarRing R] {r : R → R → Prop} (hr : ∀ (a b : R), r a b → r (star a) (star b)) ⦃a b : R⦄ : (ringConGen r) a b → (ringConGen r) (star a) (star b)