case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ x ^ n ∣ x ^ m → n ≤ m

case mpr
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ n ≤ m → x ^ n ∣ x ^ m
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ x ^ n ∣ x ^ m ↔ n ≤ m
constructor
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
⊢ n ≤ m
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ x ^ n ∣ x ^ m → n ≤ m
intro h
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
⊢ ¬m < n
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
⊢ n ≤ m
rw [← not_lt]
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ False
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
⊢ ¬m < n
intro hmn
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ IsUnit x
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ False
apply h1
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
this : x ^ m * x ∣ x ^ m * 1
⊢ IsUnit x
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ IsUnit x
have : x ^ m * x ∣ x ^ m * 1 := by
  rw [← pow_succ', mul_one]
  exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
this : x ^ m * x ∣ x ^ m * 1
⊢ x ^ m ≠ 0
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
this : x ^ m * x ∣ x ^ m * 1
⊢ IsUnit x
rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
no goals
case mp
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
this : x ^ m * x ∣ x ^ m * 1
⊢ x ^ m ≠ 0
apply pow_ne_zero m h0
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ x ^ (m + 1) ∣ x ^ m
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ x ^ m * x ∣ x ^ m * 1
rw [← pow_succ', mul_one]
no goals
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ x ^ (m + 1) ∣ x ^ m
exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
no goals
case mpr
R : Type u_1
S : Type ?u.68385
M : Type ?u.68388
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ n ≤ m → x ^ n ∣ x ^ m
apply pow_dvd_pow