def m01

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:32

import Base
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

32def m01(+m: Nat, +hl: {Nat.is_lt(m, 2n) == True{} : Bool}, +h: {Nat.is_eq(m, 1n) == False{} : Bool}) -> {m == 0n : Nat}:
33  match m:
34    case 0n:
35      {==}
36    case 1n+ +mp:
37      match mp:
38        case 0n:
39          NC.absurd_tf({1n == 0n : Nat}, Equal.sym(Bool, True{}, False{}, h))
40        case 1n+ +mq:
41          Empty.absurd({2n+mq == 0n : Nat}, N.lt_zero_absurd(mq, hl))