def ge_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64.bend:71

import Base

71# Nothing compares below zero.
72def ge_zero(+n: Nat, +w: Word(n)) -> {Cmp.is_ge(Word.cmp(n, w, Word.zero(n))) == True{} : Bool}:
73  match n w:
74    case 0n WNil{}:
75      {==}
76    case 1n+p WCon{x, t}:
77      ge_fin_zero(Word.cmp(p, t, Word.zero(p)), x, ge_zero(p, t))