case intro
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn : Nat.succ k ≠ 0
⊢ x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
hn : n ≠ 0
⊢ x ^ n + y ^ n ≤ (x + y) ^ n
rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
case intro.zero
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
⊢ x ^ Nat.succ Nat.zero + y ^ Nat.succ Nat.zero ≤ (x + y) ^ Nat.succ Nat.zero

case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
case intro
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn : Nat.succ k ≠ 0
⊢ x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
induction' k with k ih
case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
case intro.zero
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
⊢ x ^ Nat.succ Nat.zero + y ^ Nat.succ Nat.zero ≤ (x + y) ^ Nat.succ Nat.zero

case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
. have eqn : Nat.succ Nat.zero = 1 := rfl
  rw [eqn]
  simp only [pow_one, le_refl]
no goals
case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
. let n := k.succ
  have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
  have h2 := add_nonneg hx hy
  calc
    x ^ n.succ + y ^ n.succ ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
      rw [pow_succ _ n, pow_succ _ n]
      exact le_add_of_nonneg_right h1
    _ = (x + y) * (x ^ n + y ^ n) := by
      rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
        add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
    _ ≤ (x + y) ^ n.succ := by
      rw [pow_succ _ n]
      exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2
case intro.zero
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
eqn : Nat.succ Nat.zero = 1
⊢ x ^ Nat.succ Nat.zero + y ^ Nat.succ Nat.zero ≤ (x + y) ^ Nat.succ Nat.zero
case intro.zero
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
⊢ x ^ Nat.succ Nat.zero + y ^ Nat.succ Nat.zero ≤ (x + y) ^ Nat.succ Nat.zero
have eqn : Nat.succ Nat.zero = 1 := rfl
case intro.zero
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
eqn : Nat.succ Nat.zero = 1
⊢ x ^ 1 + y ^ 1 ≤ (x + y) ^ 1
case intro.zero
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
eqn : Nat.succ Nat.zero = 1
⊢ x ^ Nat.succ Nat.zero + y ^ Nat.succ Nat.zero ≤ (x + y) ^ Nat.succ Nat.zero
rw [eqn]
no goals
case intro.zero
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn✝ : Nat.succ k ≠ 0
hn : Nat.succ Nat.zero ≠ 0
eqn : Nat.succ Nat.zero = 1
⊢ x ^ 1 + y ^ 1 ≤ (x + y) ^ 1
simp only [pow_one, le_refl]
case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
let n := k.succ
case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
have h2 := add_nonneg hx hy
no goals
case intro.succ
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ Nat.succ (Nat.succ k) + y ^ Nat.succ (Nat.succ k) ≤ (x + y) ^ Nat.succ (Nat.succ k)
calc
  x ^ n.succ + y ^ n.succ ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) := by
    rw [pow_succ _ n, pow_succ _ n]
    exact le_add_of_nonneg_right h1
  _ = (x + y) * (x ^ n + y ^ n) := by
    rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
      add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
  _ ≤ (x + y) ^ n.succ := by
    rw [pow_succ _ n]
    exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ Nat.succ n + y ^ Nat.succ n ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
rw [pow_succ _ n, pow_succ _ n]
no goals
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)
exact le_add_of_nonneg_right h1
no goals
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)
rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
  add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) ^ Nat.succ n
rw [pow_succ _ n]
no goals
β : Type ?u.204204
A : Type ?u.204207
G : Type ?u.204210
M : Type ?u.204213
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
m : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
k✝ : ℕ
hn✝ : Nat.succ k✝ ≠ 0
k : ℕ
ih : Nat.succ k ≠ 0 → x ^ Nat.succ k + y ^ Nat.succ k ≤ (x + y) ^ Nat.succ k
hn : Nat.succ (Nat.succ k) ≠ 0
n : ℕ := Nat.succ k
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ (x + y) * (x ^ n + y ^ n) ≤ (x + y) * (x + y) ^ n
exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2