def pos52

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divv.bend:29

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

29def pos52(+n: Nat, +h: {C.fits(52n, n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}:
30  match n:
31    case 0n:
32      NC.absurd_tf({Nat.is_le(1n, 0n) == True{} : Bool}, Equal.sym(Bool, True{}, False{}, h))
33    case 1n+ +np:
34      N.zero_le(np)