Localization of natural transformations to preadditive categories

theorem CategoryTheory.Localization.liftNatTrans_zero {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (F₁ F₂ : Functor C E) (F₁' F₂' : Functor D E) [Lifting L W F₁ F₁'] [Lifting L W F₂ F₂'] [Limits.HasZeroMorphisms E] : liftNatTrans L W F₁ F₂ F₁' F₂' 0 = 0

theorem CategoryTheory.Localization.liftNatTrans_add {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [Preadditive E] (F₁ F₂ : Functor C E) (F₁' F₂' : Functor D E) [Lifting L W F₁ F₁'] [Lifting L W F₂ F₂'] (τ τ' : F₁ ⟶ F₂) : liftNatTrans L W F₁ F₂ F₁' F₂' (τ + τ') = liftNatTrans L W F₁ F₂ F₁' F₂' τ + liftNatTrans L W F₁ F₂ F₁' F₂' τ'