theorem max_left {a : ℕ} {b : ℕ} {b' : ℕ} {c : ℕ} {c' : ℕ} (h : a ≤ b * c) : a ≤ max b b' * max c c'

theorem max_right {a' : ℕ} {b : ℕ} {b' : ℕ} {c : ℕ} {c' : ℕ} (h : a' ≤ b' * c') : a' ≤ max b b' * max c c'

theorem max_ineq (a : ℕ) (a' : ℕ) (b : ℕ) (b' : ℕ) (c : ℕ) (c' : ℕ) (h : a ≤ b * c) (h' : a' ≤ b' * c') : max a a' ≤ max b b' * max c c'

theorem mul_ineq (a : ℕ) (a' : ℕ) (b : ℕ) (b' : ℕ) (c : ℕ) (c' : ℕ) (h : a ≤ b * c) (h' : a' ≤ b' * c') : a * a' ≤ b * b' * (c * c')

theorem add_ineq (a : ℕ) (a' : ℕ) (b : ℕ) (b' : ℕ) (c : ℕ) (c' : ℕ) (h : a ≤ b + c) (h' : a' ≤ b' + c') : a + a' ≤ b + b' + (c + c')