def internal_div_zero_le

import bend-mathlib@0.8.1.0/nat.bend as Nat

import Base

750def internal_div_zero_le(x: Nat) -> {True{} == Nat.is_le(0n, x) : Bool}:
751  Equal.sym(Bool, Nat.is_le(0n, x), True{}, zero_le(x))

Uses (5)