n : Nat
H : 0 < n
t : (0 + n) / n = succ (0 / n) := add_div_right 0 H
⊢ n / n = 1
n : Nat
H : 0 < n
⊢ n / n = 1
let t := add_div_right 0 H
no goals
n : Nat
H : 0 < n
t : (0 + n) / n = succ (0 / n) := add_div_right 0 H
⊢ n / n = 1
rwa [Nat.zero_add, Nat.zero_div] at t