R : Type u_1
S : Type ?u.85157
M : Type ?u.85160
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
hb : c ^ m ∣ b
ha : c ^ min n m ∣ a
⊢ c ^ min n m ∣ a + b
R : Type u_1
S : Type ?u.85157
M : Type ?u.85160
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
ha : c ^ n ∣ a
hb : c ^ m ∣ b
⊢ c ^ min n m ∣ a + b
replace ha := (pow_dvd_pow c (min_le_left n m)).trans ha
R : Type u_1
S : Type ?u.85157
M : Type ?u.85160
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
ha : c ^ min n m ∣ a
hb : c ^ min n m ∣ b
⊢ c ^ min n m ∣ a + b
R : Type u_1
S : Type ?u.85157
M : Type ?u.85160
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
hb : c ^ m ∣ b
ha : c ^ min n m ∣ a
⊢ c ^ min n m ∣ a + b
replace hb := (pow_dvd_pow c (min_le_right n m)).trans hb
no goals
R : Type u_1
S : Type ?u.85157
M : Type ?u.85160
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
ha : c ^ min n m ∣ a
hb : c ^ min n m ∣ b
⊢ c ^ min n m ∣ a + b
exact dvd_add ha hb