Mathlib: NormedRing on R ⧸ I for noncommutative R and two-sided I (not in Mathlib)

Mathlib v4.35 only has Ideal.Quotient.normedCommRing (commutative R), but Ideal.Quotient.ring and Ideal.Quotient.algebra already work for any Ring R and I : Ideal R with [I.IsTwoSided]. Copy the proof of Ideal.Quotient.semiNormedCommRing.norm_mul_le with R a SeminormedRing, replacing Ideal.Quotient.norm_mk_lt/norm_mk_le by Submodule.Quotient.norm_mk_lt (S := I) / Submodule.Quotient.norm_mk_le (S := I), and add one rw [map_mul] step. Then { seminormedRing I, Submodule.Quotient.normedAddCommGroup I with } gives a NormedRing when [IsClosed (I : Set R)] (IsClosed is a class now). { Submodule.Quotient.normedSpace I 𝕜, Ideal.Quotient.algebra 𝕜 with } gives a NormedAlgebra. CompleteSpace of the quotient is inferred automatically. Mark the section noncomputable. Application: compact operators as an Ideal (E →L[𝕜] E) (smul_mem' is hx.clm_comp c, IsTwoSided is ha.comp_clm b, closedness is isClosed_setOfPred_isCompactOperator) make the Calkin algebra a Banach algebra, so spectrum.nonempty (in Mathlib.Analysis.Normed.Algebra.GelfandFormula) gives a nonempty essential spectrum.