noncomputable def lemma_23_73_R_second (R : Type u) [Ring R] [Small.{v, u} R] (M A B : ModuleCat R) (n : ℕ) : ExtGroup_R R M (A ⊞ B) n ≃+ ExtGroup_R R M A n × ExtGroup_R R M B n