def internal_div_add_zero_r

bend-mathlib@0.8.1.0 · nat.bend:744

import Base

744def internal_div_add_zero_r(a: Nat) -> {a == Nat.add(a, 0n) : Nat}:
745  Equal.sym(Nat, Nat.add(a, 0n), a, add_zero(a))