prove 2 different inequalities with one function?

Stream: new members

[Oliver lang]

Can a function be used to prove 2 different inequalities with different input? Whenever i try to create a function where the output is either a proof for 0 ≤ a ^ 2 - 2 * a * b + b ^ 2 or 0 ≤ a ^ 2 + 2 * a * b + b ^ 2, i get an error because the functions type is the first inequality

import Mathlib.Analysis.SpecialFunctions.Log.Basic
import MIL.Common

theorem help0 : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2 := by
  calc
    a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg

theorem help1: 0 ≤ a ^ 2 + 2 * a * b + b ^ 2 := by
  calc
    a ^ 2 + 2 * a * b + b ^ 2 = (a + b) ^ 2 := by ring
    _ ≥ 0 := by apply pow_two_nonneg


example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
  have h : (0 : ℝ) < 2 := by norm_num
  apply abs_le'.mpr
  constructor
  . rw[le_div_iff h]
    have := help0 a b
    linarith
  . rw[le_div_iff h]
    have := help1 a b
    linarith

i want to replace the help0 and 1 with a single function basically

[Markus Schmaus]

Try to create a #mwe, this will make it easier for people to understand what exactly you are asking, and increase your probability of getting an answer.