def m10

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

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

43def m10(+m: Nat, +hl: {Nat.is_lt(m, 2n) == True{} : Bool}, +h: {Nat.is_eq(m, 0n) == False{} : Bool}) -> {m == 1n : Nat}:
44  match m:
45    case 0n:
46      NC.absurd_tf({0n == 1n : Nat}, Equal.sym(Bool, True{}, False{}, h))
47    case 1n+ +mp:
48      match mp:
49        case 0n:
50          {==}
51        case 1n+ +mq:
52          Empty.absurd({2n+mq == 1n : Nat}, N.lt_zero_absurd(mq, hl))