def internal_div_le_refl

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

import Base

747def internal_div_le_refl(a: Nat) -> {True{} == Nat.is_le(a, a) : Bool}:
748  Equal.sym(Bool, Nat.is_le(a, a), True{}, le_refl(a))

Uses (5)