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')