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