case h
α : Type ?u.174271
β : Type ?u.174274
γ : Type ?u.174277
δ : Type ?u.174280
σ : Type ?u.174283
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
m n : ℕ
⊢ (m, n).fst = m % n + (m, n).snd * (fun x x_1 => x / x_1) (m, n).fst (m, n).snd
α : Type ?u.174271
β : Type ?u.174274
γ : Type ?u.174277
δ : Type ?u.174280
σ : Type ?u.174283
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
m n : ℕ
⊢ (m, n).fst - (m, n).snd * (fun x x_1 => x / x_1) (m, n).fst (m, n).snd = m % n
apply Nat.sub_eq_of_eq_add
no goals
case h
α : Type ?u.174271
β : Type ?u.174274
γ : Type ?u.174277
δ : Type ?u.174280
σ : Type ?u.174283
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
m n : ℕ
⊢ (m, n).fst = m % n + (m, n).snd * (fun x x_1 => x / x_1) (m, n).fst (m, n).snd
simp [add_comm (m % n), Nat.div_add_mod]