case mp
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l → (x + 1) ^ k ≤ (x + 1) ^ l

case mpr
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ≤ (x + 1) ^ l → (x + 1) ^ k ∣ (x + 1) ^ l
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l ↔ (x + 1) ^ k ≤ (x + 1) ^ l
constructor
case mp
k l x : ℕ
w : 0 < x + 1
a : (x + 1) ^ k ∣ (x + 1) ^ l
⊢ (x + 1) ^ k ≤ (x + 1) ^ l
case mp
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l → (x + 1) ^ k ≤ (x + 1) ^ l
intro a
no goals
case mp
k l x : ℕ
w : 0 < x + 1
a : (x + 1) ^ k ∣ (x + 1) ^ l
⊢ (x + 1) ^ k ≤ (x + 1) ^ l
exact le_of_dvd (pow_pos (succ_pos x) l) a
case mpr
k l x : ℕ
w : 0 < x + 1
a : (x + 1) ^ k ≤ (x + 1) ^ l
⊢ (x + 1) ^ k ∣ (x + 1) ^ l
case mpr
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ≤ (x + 1) ^ l → (x + 1) ^ k ∣ (x + 1) ^ l
intro a
case mpr.zero
k l : ℕ
w : 0 < zero + 1
a : (zero + 1) ^ k ≤ (zero + 1) ^ l
⊢ (zero + 1) ^ k ∣ (zero + 1) ^ l

case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
⊢ (succ x + 1) ^ k ∣ (succ x + 1) ^ l
case mpr
k l x : ℕ
w : 0 < x + 1
a : (x + 1) ^ k ≤ (x + 1) ^ l
⊢ (x + 1) ^ k ∣ (x + 1) ^ l
cases' x with x
no goals
case mpr.zero
k l : ℕ
w : 0 < zero + 1
a : (zero + 1) ^ k ≤ (zero + 1) ^ l
⊢ (zero + 1) ^ k ∣ (zero + 1) ^ l
simp
case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
le : k ≤ l
⊢ (succ x + 1) ^ k ∣ (succ x + 1) ^ l
case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
⊢ (succ x + 1) ^ k ∣ (succ x + 1) ^ l
have le := (pow_le_iff_le_right (Nat.le_add_left _ _)).mp a
case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
le : k ≤ l
⊢ (succ x + 1) ^ l = (succ x + 1) ^ k * (x + 2) ^ (l - k)
case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
le : k ≤ l
⊢ (succ x + 1) ^ k ∣ (succ x + 1) ^ l
use (x + 2) ^ (l - k)
no goals
case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
le : k ≤ l
⊢ (succ x + 1) ^ l = (succ x + 1) ^ k * (x + 2) ^ (l - k)
rw [← pow_add, add_comm k, tsub_add_cancel_of_le le]