For non-negative integers, the product of max and min recovers a·b, and the difference of their squares factors as (max − min)(a + b)

Enuntiatio — the claim

For non-negative integers, the product of max and min recovers a·b, and the difference of their squares factors as (max − min)(a + b)

Refuted by Exhibiting non-negative integers a, b where (max(a,b) - min(a,b)) * (a + b) differs from max(a,b)^2 - min(a,b)^2, or where max(a,b)*min(a,b) != a*b.

Expressio — the formal statement

import Mathlib.Tactic

theorem minmax_law_1d72941c6314 : ∀ (a b : ℤ), (0 ≤ a) → (0 ≤ b) → ((a ≥ 0) ∧ (b ≥ 0)) → (((((max a b) - (min a b)) * (a + b)) = (((max a b) ^ (2 : ℕ)) - ((min a b) ^ (2 : ℕ)))) ∧ (((max a b) * (min a b)) = (a * b)))

Demonstratio — the kernel-checked proof

by
  intro a b _ _ _
  refine ⟨?_, ?_⟩ <;>
  (rcases le_total a b with h0 | h0 <;>
    simp only [max_eq_left, max_eq_right, min_eq_left, min_eq_right, h0] <;>
    ring)