case mp
a b r q : Int
h : 0 < b
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < b

case mpr
a b r q : Int
h : 0 < b
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < b → a / b = q ∧ a % b = r
a b r q : Int
h : 0 < b
⊢ a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b
constructor
case mp
a b r q : Int
h : 0 < b
⊢ a % b + b * (a / b) = a ∧ 0 ≤ a % b ∧ a % b < b
case mp
a b r q : Int
h : 0 < b
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < b
intro ⟨rfl, rfl⟩
no goals
case mp
a b r q : Int
h : 0 < b
⊢ a % b + b * (a / b) = a ∧ 0 ≤ a % b ∧ a % b < b
exact ⟨emod_add_ediv a b, emod_nonneg _ (Int.ne_of_gt h), emod_lt_of_pos _ h⟩
case mpr
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r
case mpr
a b r q : Int
h : 0 < b
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < b → a / b = q ∧ a % b = r
intro ⟨rfl, hz, hb⟩
case mpr.left
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) / b = q

case mpr.right
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) % b = r
case mpr
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r
constructor
case mpr.left
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ 0 + q = q
case mpr.left
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) / b = q
rw [Int.add_mul_ediv_left r q (Int.ne_of_gt h), ediv_eq_zero_of_lt hz hb]
no goals
case mpr.left
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ 0 + q = q
simp [Int.zero_add]
no goals
case mpr.right
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) % b = r
rw [add_mul_emod_self_left, emod_eq_of_lt hz hb]