def nat.le_refl

bend-osdev-algo@0.1.0.0 · PROOF.bend:91

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF

import Base

91def nat.le_refl(x: Nat) -> {Nat.is_le(x, x) == True{} : Bool}:
92  match x:
93    case 0n:
94      {==}
95    case 1n+p:
96      nat.le_refl(p)

Uses (3)

Used by (2)