feat(analysis/normed_space/normed_group_hom): add norm_noninc.neg (#9658

)

From LTE.

src/analysis/normed_space/normed_group_hom.lean

@@ -548,6 +548,9 @@ lemma comp {g : normed_group_hom V₂ V₃} {f : normed_group_hom V₁ V₂}
   (g.comp f).norm_noninc :=
 λ v, (hg (f v)).trans (hf v)
 
+@[simp] lemma neg_iff {f : normed_group_hom V₁ V₂} : (-f).norm_noninc ↔ f.norm_noninc :=
+⟨λ h x, by { simpa using h x }, λ h x, (norm_neg (f x)).le.trans (h x)⟩
+
 end norm_noninc
 
 section isometry