a : Int
H : a ≠ 0
this : div (1 * a) a = 1
⊢ div a a = 1
a : Int
H : a ≠ 0
⊢ div a a = 1
have := Int.mul_div_cancel 1 H
no goals
a : Int
H : a ≠ 0
this : div (1 * a) a = 1
⊢ div a a = 1
rwa [Int.one_mul] at this