def le_refl

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:58

import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as Nat

import Base

58def le_refl(+n: Nat) -> {Nat.is_le(n, n) == True{} : Bool}:
59  match n:
60    case 0n:
61      {==}
62    case 1n+p:
63      le_refl(p)

Uses (3)

Used by (59)