def ncmp_refl

bend-kit-collections@0.1.4.1 · PROOF.bend:3945

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF

import Base

3945def ncmp_refl(n: Nat) -> {Nat.cmp(n, n) == EQ{} : Cmp}:
3946  match n:
3947    case 0n:
3948      {==}
3949    case 1n+p:
3950      ncmp_refl(p)

Uses (3)

Used by (1)

bend-kit-collections@0.1.4.1/PROOF:ucmp_refl